diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-07 16:01:27 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:17 +0100 |
| commit | 33c0d3b95bdf0ff1fdd2d6dbe7088e48c2fa6f67 (patch) | |
| tree | eeb59c03cde25626ba674cebe6f6b123d814e0af /doc | |
| parent | 43816ce712054c07cb04452821570054aff3dc44 (diff) | |
GRAMMAR: added punctuation
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 2a4ccfed8..092dba46b 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1738,7 +1738,7 @@ The first stage is to precise on which argument the fixpoint will be decreasing. The type of this argument should be an inductive definition. -For doing this the syntax of fixpoints is extended and becomes +For doing this, the syntax of fixpoints is extended and becomes \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\] where $k_i$ are positive integers. Each $A_i$ should be a type (reducible to a term) starting with at least |