From 2cb48a3fe5a8cd435e4e0ad6990e5ee5e6079fa5 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sat, 7 Nov 2015 16:17:44 +0100 Subject: COMMENT: to do --- doc/refman/RefMan-cic.tex | 2 ++ 1 file changed, 2 insertions(+) (limited to 'doc/refman/RefMan-cic.tex') 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 -- cgit v1.2.3