def String.mangle (s : String) : String

Equations

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

@[export lean_name_mangle]

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

Equations

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

@[export lean_mk_module_initialization_function_name]

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

Equations

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