diff options
| author | Matej Kosik | 2015-11-07 18:06:41 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:17 +0100 |
| commit | 02be0f4e071c12800177eecdb067949dcce3b174 (patch) | |
| tree | 8d3cc9830f908198e32335dc18f61cb6fb8e994d /doc | |
| parent | fc8e19c82a24fea551b47a99bb68f6f64fc16a01 (diff) | |
COMMENT: question
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 8c8537cfb2..1a17f3f35f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1764,7 +1764,9 @@ $\forall p_1:P_1,\ldots \forall p_r:P_r, \forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots p_r~t_1\ldots t_s)$ the recursive arguments will correspond to $T_i$ in which one of the $I_l$ occurs. - +% QUESTION: The last sentence above really fully make sense. +% Isn't some word missing? +% Maybe "if"? The main rules for being structurally smaller are the following:\\ Given a variable $y$ of type an inductive |