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.

def allNamesByModule (p : Lean.Name → Bool) : Lean.CoreM (Std.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.

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

Decapitalize the last component of a name.

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

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

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

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