diff options
| -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 51a0068b03..bacd62b776 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -999,6 +999,7 @@ provided that the following side conditions hold: $I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots I_k$ and $c_i \notin \Gamma \cup E$. \end{itemize} +% TODO: justify the above constraints \end{description} One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its |