Documentation

Lean.Compiler.NameMangling

def String.mangle (s : String) :

Equations

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

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

Equations

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

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

Equations

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