def String.mangle (s : String) : String

@[export lean_name_mangle]

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

@[export lean_mk_module_initialization_function_name]

def Lean.mkModuleInitializationFunctionName (moduleName : Name) : String