mathlib documentation

core / init.meta.occurrences

inductive occurrences :

Type

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.

def occurrences.contains :

occurrences → ℕ → bool

Equations

(occurrences.neg ps).contains p = to_bool (p ∉ ps)
(occurrences.pos ps).contains p = to_bool (p ∈ ps)
occurrences.all.contains p = tt

@[protected, instance]

def occurrences.inhabited :

inhabited occurrences

Equations

occurrences.inhabited = {default := occurrences.all}

def occurrences_repr :

occurrences → string

Equations

occurrences_repr (occurrences.neg l) = "-" ++ repr l
occurrences_repr (occurrences.pos l) = repr l
occurrences_repr occurrences.all = "*"

@[protected, instance]

def occurrences.has_repr :

has_repr occurrences

Equations

occurrences.has_repr = {repr := occurrences_repr}

meta def occurrences_to_format :

occurrences → format

@[protected, instance]

meta def occurrences.has_to_format :

has_to_format occurrences