Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/InductiveTypes.v Wed Jul 25 15:07:12 2012 -0400 +++ b/src/InductiveTypes.v Wed Jul 25 15:51:54 2012 -0400 @@ -74,7 +74,7 @@ (** * Enumerations *) -(** 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. +(** 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. The singleton type [unit] is an inductive type:%\index{Gallina terms!unit}\index{Gallina terms!tt}% *)