diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-04 19:41:25 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:14 +0100 |
| commit | 760765859cb74930ac8fd14fc1a241aa8ae20aa0 (patch) | |
| tree | 1ec2dd8f6f5d2da3e3d41a8c0126bbca81234e83 | |
| parent | 5edfac63b6feb0b8d6ddad47a4ca9c8b5905b03a (diff) | |
COMMENT: question
| -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 |