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}% *)