Exercise 4.1 page 76 Some types in the calculus of constructions

Exercise 4.2 page 90 A polymorphic functional

Exercises 4.3 page 93 and 4.5 page 97 Some inference rules

Exercise 4.4 page 96 Some simple polymorphic functions

- 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 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.

Going home

Pierre Castéran