diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index dfcebf1860..20444dc0a1 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -137,18 +137,18 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := \end{coq_example} Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are -automatically generated by the pattern-matching compilation algorithm): +automatically generated by the pattern-matching compilation algorithm). \begin{coq_example} - Obligations. + Obligation 1. \end{coq_example} -You can use a well-founded order or a measure as termination orders using the syntax: +One can use a well-founded order or a measure as termination orders using the syntax: \begin{coq_eval} Reset Initial. Require Import Arith. Require Import Program. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Definition id (n : nat) := n. Program Fixpoint div2 (n : nat) {measure id n} : { x : nat | n = 2 * x \/ n = 2 * x + 1 } := @@ -156,7 +156,7 @@ Program Fixpoint div2 (n : nat) {measure id n} : | S (S p) => S (div2 p) | _ => O end. -\end{coq_example} +\end{coq_example*} The \verb|measure| keyword expects a measure function into the naturals, whereas \verb|wf| expects a relation. @@ -270,4 +270,5 @@ Program Fixpoint f (x : A | P) { measure size } := %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" +%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf" %%% End: |