diff options
| author | herbelin | 2006-12-08 10:26:54 +0000 |
|---|---|---|
| committer | herbelin | 2006-12-08 10:26:54 +0000 |
| commit | 56cf321a6a275bca6fde0cafb36b6cc9bfba0f93 (patch) | |
| tree | 6647726bdf475cc5e57ee372afbd3196fbfbbab1 /doc/refman | |
| parent | fef03cfe009efefdcfdc5ccff88d8fbadaf6feb0 (diff) | |
Correction typo règle réduction du fix chapitre CCI
Maj mode emacs coqide dans faq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 34b5a3fbf9..7183e040e1 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1572,7 +1572,8 @@ Let $F$ be the set of declarations: $f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n$. The reduction for fixpoints is: \[ (\Fix{f_i}{F}~a_1\ldots -a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n}\] +a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n} +~a_1\ldots a_{k_i}\] when $a_{k_i}$ starts with a constructor. This last restriction is needed in order to keep strong normalization and corresponds to the reduction for primitive recursive operators. |