From e16bbf716b97128272556134b88da2e80c3d115d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Fri, 8 Jan 2021 12:06:24 -0800 Subject: Improve doc of occurrences and rewrite. --- doc/sphinx/proof-engine/tactics.rst | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/proof-engine') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 766f7ab44e..25efca563a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -498,10 +498,16 @@ one or more of its hypotheses. :n:`{? - } {+ @nat_or_var }` Selects the specified occurrences within a single goal or hypothesis. - Occurrences are numbered from left to right starting with 1 when the - goal is printed with the :flag:`Printing All` flag. (In particular, occurrences - in :ref:`implicit arguments ` and - :ref:`coercions ` are counted but not shown by default.) + Occurrences are numbered starting with 1 following a depth-first traversal + of the term's expression, including occurrences in + :ref:`implicit arguments ` + and :ref:`coercions ` that are not displayed by default. + (Set the :flag:`Printing All` flag to show those in the printed term.) + + For example, when matching the pattern `_ + _` in the term `(a + b) + c`, + occurrence 1 is `(...) + c` and + occurrence 2 is `(a + b)`. When matching that pattern with term `a + (b + c)`, + occurrence 1 is `a + (...)` and occurrence 2 is `b + c`. Specifying `-` includes all occurrences *except* the ones listed. -- cgit v1.2.3