def String.mangle (s : String) : String

def Lean.Name.mangle (n : Name) (pre : String := "l_") : String

@[export lean_mk_mangled_boxed_name]

def Lean.mkMangledBoxedName (s : String) : String

Given s = nm.mangle pre for some nm : Name and pre : String with nm != Name.anonymous, returns (mkBoxedName nm).mangle pre. This is used in the interpreter to find names of boxed IR declarations.

def Lean.mkModuleInitializationStem (moduleName : Name) (pkg? : Option PkgId := none) : String

The mangled name of the name used to create the module initialization function.

This also used for the library name of a module plugin.

def Lean.mkModuleInitializationFunctionName (moduleName : Name) (pkg? : Option PkgId := none) : String

def Lean.mkPackageSymbolPrefix (pkg? : Option PkgId) : String

def Lean.Name.demangle (s : String) : Name

Assuming s has been produced by Name.mangle _ "", return the original name.

def Lean.Name.demangle? (s : String) : Option Name

Returns the demangled version of s, if it's the result of Name.mangle _ "". Otherwise returns none.