diff options
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 73 |
1 files changed, 64 insertions, 9 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index f25497179..d713661c2 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -141,17 +141,11 @@ is understood as & | & {\tt constr :} {\term}\\ & | & {\tt uconstr :} {\term}\\ & | & {\tt type\_term} {\term}\\ +& | & {\tt numgoals} \\ +& | & {\tt guard} {\it test}\\ & | & \atomictac\\ & | & {\qualid} \nelist{\tacarg}{}\\ -& | & {\atom}\\ -\\ -{\atom} & ::= & - {\qualid} \\ -& | & ()\\ -& | & {\integer}\\ -& | & {\tt (} {\tacexpr} {\tt )}\\ -\\ -{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ +& | & {\atom} \end{tabular} \end{centerframe} \caption{Syntax of the tactic language} @@ -163,6 +157,14 @@ is understood as \begin{figure}[htbp] \begin{centerframe} \begin{tabular}{lcl} +{\atom} & ::= & + {\qualid} \\ +& | & ()\\ +& | & {\integer}\\ +& | & {\tt (} {\tacexpr} {\tt )}\\ +\\ +{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ +\\ \tacarg & ::= & {\qualid}\\ & $|$ & {\tt ()} \\ @@ -186,6 +188,13 @@ is understood as & $|$ & {\tt appcontext} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ & $|$ & {\tt \_ =>} {\tacexpr}\\ +\\ +{\it test} & ::= & + {\integer} {\tt \,=\,} {\integer}\\ +& $|$ & {\integer} {\tt \,<\,} {\integer}\\ +& $|$ & {\integer} {\tt <=} {\integer}\\ +& $|$ & {\integer} {\tt \,>\,} {\integer}\\ +& $|$ & {\integer} {\tt >=} {\integer} \end{tabular} \end{centerframe} \caption{Syntax of the tactic language (continued)} @@ -887,6 +896,52 @@ term which can be used in tactics. {\tt type\_term} {\term} \end{quote} +\subsubsection[Counting the goals]{Counting the goals\index{Ltac!numgoals}\index{numgoals!in Ltac}} + +The number of goals under focus can be recovered using the {\tt + numgoals} function. Combined with the {\tt guard} command below, it +can be used to branch over the number of goals produced by previous tactics. + +%% spiwack: could be a reasonable example, but unfortunately it turns out +%% to be more confusing than anything. +%% \begin{coq_example*} +%% Ltac pr_numgoals := let n := numgoals in idtac n. + +%% Goal True /\ True /\ True. +%% split;[|split]. +%% \end{coq_example*} +%% \begin{coq_example} +%% all:pr_numgoals. +%% \end{coq_example} + +\subsubsection[Testing boolean expressions]{Testing boolean expressions\index{Ltac!guard}\index{guard!in Ltac}} + +The {\tt guard} tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds without affecting the proof. + +\begin{quote} +{\tt guard} {\it test} +\end{quote} + +The accepted tests are simple integer comparisons. + +\begin{coq_example*} +Goal True /\ True /\ True. +split;[|split]. +\end{coq_example*} +\begin{coq_example} +all:let n:= numgoals in guard n<4. +Fail all:let n:= numgoals in guard n=2. +\end{coq_example} +\begin{ErrMsgs} + +\item \errindex{Condition not satisfied} + +\end{ErrMsgs} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + \subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract} \index{Tacticals!abstract@{\tt abstract}}} |