HepLean Documentation
Lean
.
Compiler
.
NameMangling
Search
Google site search
return to top
source
Imports
Lean.Data.Name
Imported by
String
.
mangle
Lean
.
Name
.
mangle
Lean
.
mkModuleInitializationFunctionName
source
def
String
.
mangle
(s :
String
)
:
String
Equations
s
.mangle
=
String.mangleAux
s
.length
s
.mkIterator
""
Instances For
source
@[export lean_name_mangle]
def
Lean
.
Name
.
mangle
(n :
Lean.Name
)
(pre :
String
:=
"l_"
)
:
String
Equations
n
.mangle
pre
=
pre
++
Lean.Name.mangleAux
n
Instances For
source
@[export lean_mk_module_initialization_function_name]
def
Lean
.
mkModuleInitializationFunctionName
(moduleName :
Lean.Name
)
:
String
Equations
Lean.mkModuleInitializationFunctionName
moduleName
=
"initialize_"
++
moduleName
.mangle
""
Instances For