Definitions/proofs completed in Basics.v:
- Fixpoint incr
- Definition bin_to_nat (was Fixpoint in original text)
- Example test_bin_incr1
- Example test_bin_incr6
Definitions/proofs completed in Induction.v:
- Theorem mul_0_r
- Fixpoint incr
- Fixpoint bin_to_nat
- Theorem bin_to_nat_pres_incr
- Fixpoint nat_to_bin
- Theorem nat_bin_nat
Notes for Lists.v
- bin_nat_bin
- notation (lists)
- app, alternate
- (skip) bags
- Search
- rev_length, app_length
- rev_involutive
- involution_injective
- rev_injective
- partial_map, find, update_eq, update_neq
Notes for Poly.v
- general polymorphism
- (same) rev_app_distr, rev_involutive
- split
- anon function, higher-order arguments
- map_rev
- fold, fold_length, fold_map
- partial application
- church numerals