def String.mangle (s : String) : String

Equations

• String.mangle s = String.mangleAux (String.length s) (String.mkIterator s) ""

@[export lean_name_mangle]

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

Equations

• Lean.Name.mangle n pre = pre ++ Lean.Name.mangleAux n

@[export lean_mk_module_initialization_function_name]

def Lean.mkModuleInitializationFunctionName (moduleName : Lake.Name) : String

Equations

• Lean.mkModuleInitializationFunctionName moduleName = "initialize_" ++ Lean.Name.mangle moduleName ""