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