Dependent Products

All the examples of the chapter

Exercises

Errata

• Page 84, (first paragraph)
  Read "the last argument should be an integer of the type Z, but it is an element of nat that is provided"
• Page 92, Fig 4.4, remove the mention "simple types"
• Page 99, "in other words, if gives a type to type constructors" should be "in other words, it gives a type to type constructors"
• Page 102 (list of typing judgments) :

   list (Z -> nat) : Set
   cons (A:= Z-> nat) : (Z->nat) ->
                        list (Z -> nat) ->
                        list (Z -> nat)
   cons Zabs_nat : list (Z -> nat)
   

  
  Notice that Zabs_nat is the |.| function.