diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-09 16:52:23 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:19 +0100 |
| commit | 5e48f1aafb45d1c883e32e13a8458979663b04fb (patch) | |
| tree | fe593e8ab9c9de25859051e01e654b564bed40a0 /doc | |
| parent | 15311e51c20e6edc3b97f12d483dd15bfbc1164c (diff) | |
PROPOSITION: Added "if" and "then" words missing in the original sentence.
Diffstat (limited to 'doc')
| -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:\\ |