diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:25:04 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:56:52 +0200 |
commit | 5f9b15657dacd258fbd9084424afd4aa96929f3f (patch) | |
tree | c64620479d3a24e5e6c65fd40050ae4cf86ea6c4 /doc/refman | |
parent | afa441019432f70245fed6adc5eb0318514e4357 (diff) |
Documentation: a simple example for [numgoals].
Now that [idtac] can print a single message for several goals, printing the number of goals is readable.
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-ltac.tex | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 49b0cadf0..13ff9afb1 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -914,17 +914,15 @@ 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} +\begin{coq_example*} +Ltac pr_numgoals := let n := numgoals in idtac "There are" n "goals". + +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}} |