# HG changeset patch # User Adam Chlipala # Date 1358685335 18000 # Node ID 88688402dc824dc9c5d8e3eb69f5be32c13323c1 # Parent b7419a10e52eac9b752d7b75e3bb18d52af64739 Pass through Chapter 7 diff -r b7419a10e52e -r 88688402dc82 src/GeneralRec.v --- a/src/GeneralRec.v Sun Jan 20 06:59:34 2013 -0500 +++ b/src/GeneralRec.v Sun Jan 20 07:35:35 2013 -0500 @@ -901,7 +901,7 @@ Error: Universe inconsistency. >> -The problem has to do with rules for inductive definitions that we still study in more detail in Chapter 12. Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B]. To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat]. However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined. Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *) +The problem has to do with rules for inductive definitions that we will study in more detail in Chapter 12. Briefly, recall that the type of the constructor [Bnd] quantifies over a type [B]. To make [testCurriedAdd] work, we would need to instantiate [B] as [nat -> comp nat]. However, Coq enforces a %\emph{predicativity restriction}% that (roughly) no quantifier in an inductive or co-inductive type's definition may ever be instantiated with a term that contains the type being defined. Chapter 12 presents the exact mechanism by which this restriction is enforced, but for now our conclusion is that [comp] is fatally flawed as a way of encoding interesting higher-order functional programs that use general recursion. *) (** * Comparing the Alternatives *)