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 : Lean.Name) : Lean.Name

Decapitalize the last component of a name.

Equations

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