Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 488:31258618ef73
Incorporate feedback from Nathan Collins
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Tue, 08 Jan 2013 14:38:56 -0500 |
| parents | 1fd4109f7b31 |
| children | 4a663981b699 |
comparison
equal
deleted
inserted
replaced
| 487:8bfb27cf0121 | 488:31258618ef73 |
|---|---|
| 505 P (Nil T) -> | 505 P (Nil T) -> |
| 506 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> | 506 (forall (t : T) (l : list T), P l -> P (Cons t l)) -> |
| 507 forall l : list T, P l | 507 forall l : list T, P l |
| 508 ]] | 508 ]] |
| 509 | 509 |
| 510 Thus, even though we just saw that [T] is added as an extra argument to the constructor [Cons], the inductive case in the type of [list_ind] (i.e., the third line of the type) includes no quantifier for [T], even though all of the other arguments are quantified explicitly. Parameters in other inductive definitions are treated similarly in stating induction principles. *) | 510 Thus, despite a very real sense in which the type [T] is an argument to the constructor [Cons], the inductive case in the type of [list_ind] (i.e., the third line of the type) includes no quantifier for [T], even though all of the other arguments are quantified explicitly. Parameters in other inductive definitions are treated similarly in stating induction principles. *) |
| 511 | 511 |
| 512 | 512 |
| 513 (** * Mutually Inductive Types *) | 513 (** * Mutually Inductive Types *) |
| 514 | 514 |
| 515 (** We can define inductive types that refer to each other: *) | 515 (** We can define inductive types that refer to each other: *) |