# 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

- p. 383, lines 22 and 24: 'integer' should be 'natural number'
- Page 389, sixth line

Read "forall (b_{1}:t'_{1})...(b_{l}:t'_{l}), f (c b_{i1} b_{ik})"
- Page 398, (3rd paragraph of 14.2.3),

Read "R a_{i+1} a_{i}" instead of
"R a_{i} a_{i+1}"
*Id*:

The correct definition is:

` forall x, (forall y, R y x -> Phi y) <-> Phi x `

Going home

Pierre Castéran