diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 37ca23417d..1781d96fe5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1098,6 +1098,8 @@ we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots n}$; \end{itemize} \end{description} +% QUESTION: Do we need the following paragraph? +% (I find it confusing.) Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf Ind-Const} and {\bf App}, then it is typable using the rule {\bf Ind-Family}. Conversely, the extended theory is not stronger than the @@ -1206,6 +1208,8 @@ Because we need to keep a consistent theory and also we prefer to keep a strongly normalizing reduction, we cannot accept any sort of recursion (even terminating). So the basic idea is to restrict ourselves to primitive recursive functions and functionals. +% TODO: it may be worthwhile to show the consequences of lifting +% those restrictions. For instance, assuming a parameter $A:\Set$ exists in the local context, we want to build a function \length\ of type $\ListA\ra \nat$ which @@ -1929,6 +1933,14 @@ impredicative system for sort \Set{} become: % % Inductive foo (A:Type) : Type := % | foo1 : foo A +% +% then Coq claims that 'foo' has type 'Type → Prop'. +% Why? + +% QUESTION: If I add this definition: +% +% Inductive foo (A:Type) : Type := +% | foo1 : foo A % | foo2 : foo A. % % then Coq claims that 'foo' has type 'Type → Set'. |