Foundations of Inductive Types

The complete source of examples from this chapter click here

Exercises


Exercise 14.1 page 392 A direct definition of addition
Exercise 14.4 page 394 Using maximal induction principles (le)
Exercise 14.5 page 396 About Left Factors
Exercise 14.6 page 398 eq_rec as an identity function
Exercise 14.7 page 405 A correct induction principle for lists of trees
Exercise 14.8 page 405 A counting function for trees and lists of trees
Exercise 14.9 page 406 A counting function for trees and lists of trees (cont.)

Errata

  1. p. 383, lines 22 and 24: 'integer' should be 'natural number'
  2. Page 389, sixth line
    Read "forall (b1:t'1)...(bl:t'l), f (c bi1 bik)"
  3. Page 398, (3rd paragraph of 14.2.3),
    Read "R ai+1 ai" instead of "R ai ai+1"
  4. Id:
    The correct definition is:
    forall x, (forall y, R y x -> Phi y) <-> Phi x



Going home
Pierre Castéran