diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2021-03-08 11:48:20 -0800 |
| commit | 0d33024ff79c38d52fde49e23d0e45d9c22eefbe (patch) | |
| tree | 864068cd317abebcbc0a3466a1365258729fbc40 /doc/sphinx/proof-engine/tactics.rst | |
| parent | fb0666d50e1fe95ad2325f4ef2cc9fdd2666ac8a (diff) | |
Convert 2nd part of rewriting chapter to prodn
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 |