diff options
| author | Matej Kosik | 2015-11-07 17:30:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:17 +0100 |
| commit | fc8e19c82a24fea551b47a99bb68f6f64fc16a01 (patch) | |
| tree | f3ffdc42b1c8eb0743119536141b93b037161a30 /doc | |
| parent | 2cb48a3fe5a8cd435e4e0ad6990e5ee5e6079fa5 (diff) | |
COMMENT: question
Diffstat (limited to 'doc')
| -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 |