diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b862db320..9e49481e2 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1007,6 +1007,7 @@ constructors which will always be satisfied for the impredicative sort {\Prop} but may fail to define inductive definition on sort \Set{} and generate constraints between universes for inductive definitions in the {\Type} hierarchy. +% QUESTION: which 'constraint' are we above referring to? \paragraph{Examples.} It is well known that existential quantifier can be encoded as an |