The Author Online Book Forums are Moving

The Author Online Book Forums will soon redirect to Manning's liveBook and liveVideo. All book forum content will migrate to liveBook's discussion forum and all video forum content will migrate to liveVideo. Log in to liveBook or liveVideo with your Manning credentials to join the discussion!

Thank you for your engagement in the AoF over the years! We look forward to offering you a more enhanced forum experience.

maczniak (2) [Avatar] Offline
I found this in the final PDF version.

In Listing 13.1, the
data DoorCmd : Type where
line should be
data DoorCmd : Type -> Type where
. In fact, this code is not in Door.idr file. Door.idr contains an updated version (Listing 13.2).

And there is a strange thing in Listing 13.8 (section 13.2.2, page 366). Two comments ("The length of the output vector is the output height of the stack.") are the same. I guess that the below one might be different.