fad0e69cc7
This PR fixes name mangling to be unambiguous / injective by adding `00` for disambiguation where necessary. Additionally, the inverse function, `Lean.Name.unmangle` has been added which can be used to unmangle a mangled identifier. This unmangler has been added to demonstrate the injectivity but also to allow unmangling identifiers e.g. for debugging purposes. Closes #10724
12 lines
252 B
Text
12 lines
252 B
Text
import Lean
|
|
def main : IO Unit := pure () /- -- TODO: remove after stage0 update
|
|
|
|
open Lean
|
|
|
|
def main : IO UInt32 := do
|
|
let e := mkAppN (mkConst `f) #[mkConst `a, mkConst `b]
|
|
IO.println e
|
|
IO.println s!"hash: {e.hash}"
|
|
IO.println e.getAppArgs
|
|
pure 0
|
|
-/
|