diff options
| author | Matej Kosik | 2015-11-04 19:24:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:14 +0100 |
| commit | d62af5e39af63387f60dd0a92d9fbfd65974fcae (patch) | |
| tree | a69550b115bbe4c649c4068438f82451b5e8851f /doc/refman | |
| parent | 1200468d82136ab3279bbe18da8fa0ba4e4cc8c4 (diff) | |
COMMENT: to do
Diffstat (limited to 'doc/refman')
| -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 |