Additional functions on Lean.Name.

We provide allNames and allNamesByModule.

def allNames (p : Lean.Name → Bool) : Lean.CoreM (Array Lean.Name)

Retrieve all names in the environment satisfying a predicate.

Equations

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

def allNamesByModule (p : Lean.Name → Bool) : Lean.CoreM (Batteries.HashMap Lean.Name (Array Lean.Name))

Retrieve all names in the environment satisfying a predicate, gathered together into a HashMap according to the module they are defined in.

Equations

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

def Lean.Name.decapitalize (n : Lean.Name) : Lean.Name

Decapitalize the last component of a name.

Equations

• n.decapitalize = n.modifyBase fun (x : Lean.Name) => match x with | p.str s => p.str s.decapitalize | n => n

def Lean.Name.isAuxLemma (n : Lean.Name) : Bool

Whether the lemma has a name of the form produced by Lean.Meta.mkAuxLemma.

Equations

• n.isAuxLemma = match n with | (pre.str "_auxLemma").num i => true | x => false

def Lean.Meta.unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr

Unfold all lemmas created by Lean.Meta.mkAuxLemma. The names of these lemmas end in _auxLemma.nn where nn is a number.

Equations

• Lean.Meta.unfoldAuxLemmas e = liftM (Lean.Meta.deltaExpand e Lean.Name.isAuxLemma)