mathlib documentation

core / init.meta.occurrences

inductive occurrences  :
Type

We can specify the scope of application of some tactics using the following type.

  • all : all occurrences of a given term are considered.

  • pos [1, 3] : only the first and third occurrences of a given term are consiered.

  • neg [2] : all but the second occurrence of a given term are considered.