diff options
Diffstat (limited to 'doc/refman/Program.tex')
| -rw-r--r-- | doc/refman/Program.tex | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 723936f5b9..ea694f61d2 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -137,6 +137,21 @@ automatically generated by the pattern-matching compilation algorithm): Obligations. \end{coq_example} +You can use a well-founded order or a measure as termination orders using the syntax: +\begin{coq_eval} +Reset Initial. +Require Import Arith. +\end{coq_eval} +\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 } := + match n with + | S (S p) => S (div2 p) + | _ => O + end. +\end{coq_example} + \subsection{\tt Program Lemma {\ident} : type. \comindex{Program Lemma} \label{ProgramLemma}} @@ -151,10 +166,16 @@ The following commands are available to manipulate obligations: \begin{itemize} \item {\tt Obligations [of \ident]} Displays all remaining obligations. -\item {\tt Solve Obligation num [of \ident]} Start the proof of +\item {\tt Next Obligation [of \ident]} Start the proof of the next + unsolved obligation. +\item {\tt Obligation num [of \ident]} Start the proof of obligation {\tt num}. \item {\tt Solve Obligations [of \ident] using} {\tacexpr} Tries to solve each obligation using the given tactic. +\item {\tt Admit Obligations [of \ident]} Admits all + obligations (does not work with structurally recursive programs). +\item {\tt Obligations Tactic := \expr} Sets the default obligation + solving tactic applied to all obligations. \end{itemize} |