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. Page 398, (3rd paragraph of 14.2.3),
    Read "R ai+1 ai" instead of "R ai ai+1"
  2. Id:
    The correct definition is:
    forall x, (forall y, R y x -> Phi y) <-> Phi x


Going home
Pierre Castéran