diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/faq/FAQ.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 8495156ca1..b03aa64090 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -755,19 +755,19 @@ the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}). E.g. in this case (this occurs only in the {\tt Set}-impredicative variant of \Coq): -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - \begin{coq_example*} Inductive I : Type := intro : forall k:Set, k -> I. -Lemma eq_jdef : +Lemma eq_jdef : forall x y:nat, intro _ x = intro _ y -> x = y. Proof. intros x y H; injection H. \end{coq_example*} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + Injectivity of constructors is restricted to predicative types. If injectivity on large inductive types were not restricted, we would be allowed to derive an inconsistency (e.g. following the lines of |