diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 071fcbee11..fad02b2645 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -479,6 +479,7 @@ one or more of its hypotheses. .. prodn:: occurrences ::= at @occs_nums | in @goal_occurrences + simple_occurrences ::= @occurrences occs_nums ::= {? - } {+ @nat_or_var } nat_or_var ::= {| @natural | @ident } goal_occurrences ::= {+, @hyp_occs } {? %|- {? @concl_occs } } @@ -496,6 +497,10 @@ one or more of its hypotheses. the conclusion of the goal. The second form can select occurrences in the goal conclusion and in one or more hypotheses. + :n:`@simple_occurrences` + A semantically restricted form of :n:`@occurrences` that doesn't allow the + `at` clause anywhere within it. + :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. Occurrences are numbered starting with 1 following a depth-first traversal |