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 092dba46b4..3d56dcac60 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1745,6 +1745,8 @@ Each $A_i$ should be a type (reducible to a term) starting with at least $k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ and $B_{k_i}$ being an instance of an inductive definition. +% TODO: We should probably define somewhere explicitely, what we mean by +% "x is an instance of an inductive type I". Now in the definition $t_i$, if $f_j$ occurs then it should be applied to at least $k_j$ arguments and the $k_j$-th argument should be |