Documentation

Lean.Data.Occurrences

inductive Lean.Occurrences :

Type

instance Lean.instInhabitedOccurrences :

Inhabited Lean.Occurrences

Equations

Lean.instInhabitedOccurrences = { default := Lean.Occurrences.all }

instance Lean.instBEqOccurrences :

BEq Lean.Occurrences

Equations

Lean.instBEqOccurrences = { beq := [anonymous] }

def Lean.Occurrences.contains :

Lean.Occurrences → Nat → Bool

Equations

Lean.Occurrences.contains x x = match x, x with | Lean.Occurrences.all, x => true | Lean.Occurrences.pos idxs, idx => List.contains idxs idx | Lean.Occurrences.neg idxs, idx => !List.contains idxs idx

def Lean.Occurrences.isAll :

Lean.Occurrences → Bool

Equations

Lean.Occurrences.isAll x = match x with | Lean.Occurrences.all => true | x => false