diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-07 16:17:44 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:17 +0100 |
| commit | 2cb48a3fe5a8cd435e4e0ad6990e5ee5e6079fa5 (patch) | |
| tree | 9ac9f6c24c1acb152d20c81a17eb197944544d5f /doc/refman/RefMan-cic.tex | |
| parent | 33c0d3b95bdf0ff1fdd2d6dbe7088e48c2fa6f67 (diff) | |
COMMENT: to do
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -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 092dba46b..3d56dcac6 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 |