Here we give the. implementation of Name.toString. There is also a private implementation in Init.Meta, which we cannot import this implementation due to import hierarchy limitations.

The difference between the two versions is that the one in Init.Meta uses the String.Internal.* functions, while the one here uses the public String functions. These differ in that the latter versions have better inferred borrowing annotations, which is significant for an inner-loop function like Name.toString.

@[inline]

def Lean.Name.escapePart (s : String) (force : Bool := false) : Option String

Creates a round-trippable string name component if possible, otherwise returns none. Names that are valid identifiers are not escaped, and otherwise, if they do not contain », they are escaped.

• If force is true, then even valid identifiers are escaped.

Equations

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

@[specialize #[3]]

def Lean.Name.toStringWithSep (sep : String) (escape : Bool) (n : Name) (isToken : String → Bool := fun (x : String) => false) : String

Uses the separator sep (usually ".") to combine the components of the Name into a string. See the documentation for Name.toStringWithToken for an explanation of escape and isToken.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Name.toStringWithSep sep escape Lean.Name.anonymous isToken = "[anonymous]"
• Lean.Name.toStringWithSep sep escape (Lean.Name.anonymous.str s) isToken = Lean.Name.toStringWithSep.maybeEscape✝ escape s (isToken s)
• Lean.Name.toStringWithSep sep escape (Lean.Name.anonymous.num v) isToken = toString v
• Lean.Name.toStringWithSep sep escape (n_2.num v) isToken = Lean.Name.toStringWithSep sep escape n_2 ++ sep ++ v.repr

@[specialize #[]]

def Lean.Name.toStringWithToken (n : Name) (escape : Bool := true) (isToken : String → Bool) : String

Converts a name to a string.

• If escape is true, then escapes name components using « and » to ensure that those names that can appear in source files round trip. Names with number components, anonymous names, and names containing » might not round trip. Furthermore, "pseudo-syntax" produced by the delaborator, such as _, #0 or ?u, is not escaped.
• The optional isToken function is used when escape is true to determine whether more escaping is necessary to avoid parser tokens. The insertion algorithm works so long as parser tokens do not themselves contain « or ».

Equations

• n.toStringWithToken escape isToken = Lean.Name.toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !Lean.Name.toStringWithToken.maybePseudoSyntax✝ n) n isToken

def Lean.Name.toString (n : Name) (escape : Bool := true) : String

Converts a name to a string.

• If escape is true, then escapes name components using « and » to ensure that those names that can appear in source files round trip. Names with number components, anonymous names, and names containing » might not round trip. Furthermore, "pseudo-syntax" produced by the delaborator, such as _, #0 or ?u, is not escaped.

Equations

• n.toString escape = n.toStringWithToken escape fun (x : String) => false

instance Lean.Name.instToString : ToString Name

Equations

• Lean.Name.instToString = { toString := fun (n : Lean.Name) => n.toString }