392101 (2) [Avatar] Offline
Hi - great stuff thanks for all the hard work on both the book and the language! smilie

The code in the .zip file provided has the definition
Machine : Nat -> Nat -> Type

and listing 1.5 will make a lot more sense with that line at the top.

I also suggest renumbering the notes 1-6 of listing 1.5 as notes 2-7 and adding a new note 1 for the type
Machine : Nat -> Nat -> Type

that says something to the effect of: "This type definition is easy enough; it introduces no new type-definition concepts. But take note that the remaining types in this listing are all defined as types that are dependent on the type Machine. Try loading the listing into the REPL and then doing the :t command shown earlier in this chapter on each of the seven types."

Hey, I'm a terrible writer: Take no writing tips from me smilie

And so I just put in my 2 cents as a reader (not a writer): I really benefited from seeing the definition of Machine, and also benefited from doing those 7 :t REPLs

I had a Huge AHA moment right there in the REPL: Holy cow! Those 6 types are defined using terms dependent on the type Machine, and there is that pre-condition and post-condition stuff he was talking about before in prose, but OMG now it's Right Here In LITERAL Idris Code! AHA!!

As a reader I love having some Aha moments left by the author for me to ferret out. This is a huge Aha so I don't know, might want to flog us readers about this Aha a bit more explicitly.