aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-04 19:41:25 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:14 +0100
commit760765859cb74930ac8fd14fc1a241aa8ae20aa0 (patch)
tree1ec2dd8f6f5d2da3e3d41a8c0126bbca81234e83
parent5edfac63b6feb0b8d6ddad47a4ca9c8b5905b03a (diff)
COMMENT: question
-rw-r--r--doc/refman/RefMan-cic.tex1
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