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.willRoundTrip (n : Name) : Bool

Determines if the pretty-printed version of the given name would parse as an ident with an underlying name (via getId) equal to the original name. The pretty-printer usually escapes unparsable components of a name with «», but makes exceptions for various names with special meaning, meaning that the result does not round trip. We therefore re-check those conditions here.

This function is intended to be "safe" in that if it returns true, the name will definitely round trip. (The converse is not guaranteed.) Any deviation from this behavior is a bug which should be fixed.

Equations

• n.willRoundTrip = (!n.isAnonymous && !n.hasMacroScopes && !Lean.Name.willRoundTrip.maybePseudoSyntax✝ n && !n.isInaccessibleUserName && Lean.Name.willRoundTrip.go✝ n)