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`.

source
@[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.

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
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

Instances For

source
instance Lean.Name.instToString :
ToString Name
Equations

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