source
def String.mangle (s : String) :
String
Equations

- s.mangle = String.mangleAux✝ s.length s.mkIterator ""

Instances For

source
@[export lean_name_mangle]
def Lean.Name.mangle (n : Name) (pre : String := "l_") :
String
Equations

- n.mangle pre = pre ++ Lean.Name.mangleAux✝ n

Instances For

source
@[export lean_mk_module_initialization_function_name]
def Lean.mkModuleInitializationFunctionName (moduleName : Name) :
String
Equations

- Lean.mkModuleInitializationFunctionName moduleName = "initialize_" ++ moduleName.mangle ""

Instances For