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

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