- all : occurrences
- pos : list ℕ → occurrences
- neg : list ℕ → occurrences
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
- occurrences.has_sizeof_inst
- occurrences.inhabited
- occurrences.has_repr
- occurrences.has_to_format
Equations
- (occurrences.neg ps).contains p = decidable.to_bool (p ∉ ps)
- (occurrences.pos ps).contains p = decidable.to_bool (p ∈ ps)
- occurrences.all.contains p = bool.tt
@[protected, instance]
Equations
Equations
- occurrences_repr (occurrences.neg l) = "-" ++ repr l
- occurrences_repr (occurrences.pos l) = repr l
- occurrences_repr occurrences.all = "*"
@[protected, instance]