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 3d56dcac60..8c8537cfb2 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1747,6 +1747,8 @@ 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". +% +% QUESTION: So, $k_i$ is the index of the argument on which $f_i$ is decreasing? 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 |