# mathlibdocumentation

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.

Instances for occurrences
@[protected, instance]
Equations
Equations
@[protected, instance]
Equations
@[protected, instance]