Additional functions on Lean.Name.

We provide Name.getModule, and 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 getModule (name : Lean.Name) (s : optParam String "") : Lean.Name

Returns the very first part of a name: for Mathlib.Data.Set.Basic it returns Mathlib.

Equations

• getModule Lean.Name.anonymous s = Lean.Name.mkSimple s
• getModule (Lean.Name.num pre i) s = panic (toString "panic in `getModule`: did not expect numerical name: " ++ toString (Lean.Name.num pre i) ++ toString ".")
• getModule (Lean.Name.str pre s_1) s = getModule pre s_1