Function kernel_name_of_components 

pub fn kernel_name_of_components(components: &[&str]) -> String

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/).

Every component is a string component; a numeric Lean component cannot be told apart from a digit string by its dotted spelling, so callers holding an export resolve such names through the export’s own name table (interface::lean::reference::reference_declaration).