diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index ddd9f075ef..b862db3204 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1910,7 +1910,36 @@ impredicative system for sort \Set{} become: {\compat{I:\Set}{I\ra s}}} \end{description} +% QUESTION: Why, when I add this definition: +% +% Inductive foo : Type := . +% +% Coq claims that the type of 'foo' is 'Prop'? + +% QUESTION: If I add this definition: +% +% Inductive bar (A:Type) : Type := . +% +% then Coq claims that 'bar' has type 'Type → Prop' where I would expect 'Type → Type' with appropriate constraint. +% 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'. +% Why? + +% NOTE: If I add this definition: +% +% Inductive foo (A:Type) : Type := +% | foo1 : foo A +% | foo2 : A → foo A. +% +% then Coq claims, as expected, that: +% +% foo : Type → Type. %%% Local Variables: %%% mode: latex |