inductive Lean.Occurrences : Type

• all: Lean.Occurrences
• pos: List Nat → Lean.Occurrences
• neg: List Nat → Lean.Occurrences

instance Lean.instInhabitedOccurrences : Inhabited Lean.Occurrences

Equations

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

instance Lean.instBEqOccurrences : BEq Lean.Occurrences

Equations

• Lean.instBEqOccurrences = { beq := Lean.beqOccurrences✝ }

def Lean.Occurrences.contains : Lean.Occurrences → Nat → Bool

Equations

• One or more equations did not get rendered due to their size.

def Lean.Occurrences.isAll : Lean.Occurrences → Bool

Equations

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