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.

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.