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.