diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 49e164931..9cb52dba2 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1395,6 +1395,8 @@ $I$. s_1 \in \{\Set,\Type(j)\}, s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}} \end{description} +% QUESTION: What kind of value is represented by "x" in the "numerator"? +% There, "x" is unbound. Isn't it? The case of Inductive definitions of sort \Prop{} is a bit more complicated, because of our interpretation of this sort. The only |