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 (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.

Equations

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

def Lean.Name.decapitalize (n : Name) : 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 : Name) : Bool

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

Equations

• (p.str s).isAuxLemma = "_proof_".isPrefixOf s
• n.isAuxLemma = false

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.

Equations

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