Module name 

Hierarchical names, interned: Nat.succ is Str(Str(Anon, "Nat"), "succ"), and each distinct name is one NameId, so name equality is an integer compare.

Structs

NameId

Names

Enums

NameNode

Functions

kernel_name_of_components

The kernel spelling of a Lean name given as its hierarchical components: the name the Lean importer gives a declaration in a kernel context, each component written after /s: as a JSON string, with the kernel’s primitive identities applied (Nat, Zero, Succ, the quotient’s four, and every other Nat member under Nat/).