- 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.
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
@[instance]
Equations
Equations
- occurrences_repr (occurrences.neg l) = "-" ++ repr l
- occurrences_repr (occurrences.pos l) = repr l
- occurrences_repr occurrences.all = "*"
@[instance]