def String.mangle (s : String) : String

Equations

• s.mangle = String.mangleAux✝ s s.startValidPos ""

@[export lean_name_mangle]

def Lean.Name.mangle (n : 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 : Name) : String

Equations

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

def Lean.Name.demangle (s : String) : Name

Assuming s has been produced by Name.mangle _ "", return the original name.

Equations

• Lean.Name.demangle s = Lean.Name.demangleAux.nameStart✝ s s.startValidPos Lean.Name.anonymous

def Lean.Name.demangle? (s : String) : Option Name

Returns the demangled version of s, if it's the result of Name.mangle _ "". Otherwise returns none.

Equations

• Lean.Name.demangle? s = if Lean.Name.mangleAux✝ (Lean.Name.demangle s) = s then some (Lean.Name.demangle s) else none