def String.mangle (s : String) : String

Equations

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

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

Equations

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

@[export lean_mk_mangled_boxed_name]

def Lean.mkMangledBoxedName (s : String) : String

Given s = nm.mangle pre for some nm : Name and pre : String with nm != Name.anonymous, returns (mkBoxedName nm).mangle pre. This is used in the interpreter to find names of boxed IR declarations.

Equations

• Lean.mkMangledBoxedName s = if s.endsWith "__" = true then s ++ "_00__boxed" else s ++ "___boxed"

def Lean.mkModuleInitializationStem (moduleName : Name) (pkg? : Option PkgId := none) : String

The mangled name of the name used to create the module initialization function.

This also used for the library name of a module plugin.

Equations

• Lean.mkModuleInitializationStem moduleName pkg? = moduleName.mangle (pkg?.elim "" fun (x : Lean.PkgId) => toString (String.mangle x) ++ toString "_")

def Lean.mkModuleInitializationFunctionName (moduleName : Name) (pkg? : Option PkgId := none) : String

Equations

• Lean.mkModuleInitializationFunctionName moduleName pkg? = "initialize_" ++ Lean.mkModuleInitializationStem moduleName pkg?

def Lean.mkPackageSymbolPrefix (pkg? : Option PkgId) : String

Equations

• Lean.mkPackageSymbolPrefix pkg? = pkg?.elim "l_" fun (x : Lean.PkgId) => toString "lp_" ++ toString (String.mangle x) ++ toString "_"

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.startPos 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