Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 392:4b1242b277b2
Typo fixes
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Fri, 20 Apr 2012 12:49:47 -0400 |
| parents | d1276004eec9 |
| children | 05efde66559d |
comparison
equal
deleted
inserted
replaced
| 391:fd3f1057685c | 392:4b1242b277b2 |
|---|---|
| 231 Check bool_ind. | 231 Check bool_ind. |
| 232 (** [bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b] *) | 232 (** [bool_ind : forall P : bool -> Prop, P true -> P false -> forall b : bool, P b] *) |
| 233 | 233 |
| 234 (** That is, to prove that a property describes all [bool]s, prove that it describes both [true] and [false]. | 234 (** That is, to prove that a property describes all [bool]s, prove that it describes both [true] and [false]. |
| 235 | 235 |
| 236 There is no interesting Curry-Howard analogue of [bool]. Of course, we can define such a type by replacing [Set] by [Prop] above, but the proposition we arrive it is not very useful. It is logically equivalent to [True], but it provides two indistinguishable primitive proofs, [true] and [false]. In the rest of the chapter, we will skip commenting on Curry-Howard versions of inductive definitions where such versions are not interesting. *) | 236 There is no interesting Curry-Howard analogue of [bool]. Of course, we can define such a type by replacing [Set] by [Prop] above, but the proposition we arrive at is not very useful. It is logically equivalent to [True], but it provides two indistinguishable primitive proofs, [true] and [false]. In the rest of the chapter, we will skip commenting on Curry-Howard versions of inductive definitions where such versions are not interesting. *) |
| 237 | 237 |
| 238 | 238 |
| 239 (** * Simple Recursive Types *) | 239 (** * Simple Recursive Types *) |
| 240 | 240 |
| 241 (** The natural numbers are the simplest common example of an inductive type that actually deserves the name.%\index{Gallina terms!nat}\index{Gallina terms!O}\index{Gallina terms!S}% *) | 241 (** The natural numbers are the simplest common example of an inductive type that actually deserves the name.%\index{Gallina terms!nat}\index{Gallina terms!O}\index{Gallina terms!S}% *) |
| 658 | Truth => True | 658 | Truth => True |
| 659 | Falsehood => False | 659 | Falsehood => False |
| 660 | Conjunction f1 f2 => pformulaDenote f1 /\ pformulaDenote f2 | 660 | Conjunction f1 f2 => pformulaDenote f1 /\ pformulaDenote f2 |
| 661 end. | 661 end. |
| 662 | 662 |
| 663 (** This is a just a warm-up that does not use reflexive types, the new feature we mean to introduce. When we set our sights on first-order logic instead, it becomes very handy to give constructors recursive arguments that are functions. *) | 663 (** This is just a warm-up that does not use reflexive types, the new feature we mean to introduce. When we set our sights on first-order logic instead, it becomes very handy to give constructors recursive arguments that are functions. *) |
| 664 | 664 |
| 665 Inductive formula : Set := | 665 Inductive formula : Set := |
| 666 | Eq : nat -> nat -> formula | 666 | Eq : nat -> nat -> formula |
| 667 | And : formula -> formula -> formula | 667 | And : formula -> formula -> formula |
| 668 | Forall : (nat -> formula) -> formula. | 668 | Forall : (nat -> formula) -> formula. |