Foundations of Inductive Types
The complete source of examples from this chapter click here
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.)
- p. 383, lines 22 and 24: 'integer' should be 'natural number'
- Page 389, sixth line
Read "forall (b1:t'1)...(bl:t'l), f (c bi1 bik)"
- Page 398, (3rd paragraph of 14.2.3),
Read "R ai+1 ai" instead of
"R ai ai+1"
The correct definition is:
forall x, (forall y, R y x -> Phi y) <-> Phi x