diff options
| author | Matej Kosik | 2015-11-05 16:29:48 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:16 +0100 |
| commit | bce5332773276bca755dd47608dd13ae09016ded (patch) | |
| tree | c532850cbc16c7d8e8c92be78b665545b571a3c4 | |
| parent | d139d73949ee7ab6c070cac98f1af23431967ab0 (diff) | |
COMMENT: question
| -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 49e1649316..9cb52dba28 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 |