Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 419:686cf945dd02
Pass through StackMachine, to incorporate new coqdoc features
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 25 Jul 2012 15:51:54 -0400 |
| parents | 539ed97750bb |
| children | 671a6e7e1f29 |
comparison
equal
deleted
inserted
replaced
| 418:eda5f4eb21b4 | 419:686cf945dd02 |
|---|---|
| 72 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like most any properties of general-purpose programs. *) | 72 One of the first types we introduce will be [bool], with constructors [true] and [false]. Newcomers to Coq often wonder about the distinction between [True] and [true] and the distinction between [False] and [false]. One glib answer is that [True] and [False] are types, but [true] and [false] are not. A more useful answer is that Coq's metatheory guarantees that any term of type [bool] _evaluates_ to either [true] or [false]. This means that we have an _algorithm_ for answering any question phrased as an expression of type [bool]. Conversely, most propositions do not evaluate to [True] or [False]; the language of inductively defined propositions is much richer than that. We ought to be glad that we have no algorithm for deciding mathematical truth, since otherwise it would be clear that we could not formalize undecidable properties, like most any properties of general-purpose programs. *) |
| 73 | 73 |
| 74 | 74 |
| 75 (** * Enumerations *) | 75 (** * Enumerations *) |
| 76 | 76 |
| 77 (** Coq inductive types generalize the %\index{algebraic datatypes}%algebraic datatypes found in %\index{Haskell}%Haskell and %\index{ML}%ML. Confusingly enough, inductive types also generalize %\index{generalized algebraic datatypes}%generalized algebraic datatypes (GADT's), by adding the possibility for type dependency. Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML. | 77 (** Coq inductive types generalize the %\index{algebraic datatypes}%algebraic datatypes found in %\index{Haskell}%Haskell and %\index{ML}%ML. Confusingly enough, inductive types also generalize %\index{generalized algebraic datatypes}%generalized algebraic datatypes (GADTs), by adding the possibility for type dependency. Even so, it is worth backing up from the examples of the last chapter and going over basic, algebraic datatype uses of inductive datatypes, because the chance to prove things about the values of these types adds new wrinkles beyond usual practice in Haskell and ML. |
| 78 | 78 |
| 79 The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index{Gallina terms!tt}% *) | 79 The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index{Gallina terms!tt}% *) |
| 80 | 80 |
| 81 Inductive unit : Set := | 81 Inductive unit : Set := |
| 82 | tt. | 82 | tt. |