diff options
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index ac860b827..6c1417a7f 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1622,10 +1622,10 @@ The definition of being structurally smaller is a bit technical. One needs first to define the notion of {\em recursive arguments of a constructor}\index{Recursive arguments}. For an inductive definition \Ind{}{r}{\Gamma_I}{\Gamma_C}, -the type of a constructor $c$ has the form +if the type of a constructor $c$ has the form $\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 +p_r~t_1\ldots t_s)$, then the recursive arguments will correspond to $T_i$ in which one of the $I_l$ occurs. The main rules for being structurally smaller are the following:\\ |