max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/init/lean/name_mangling): make sure name mangling procedure behaves like the C++ one

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-20 10:23:50 -07:00
parent 3ffe0e22c8
commit 830606757b
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/lean/name_mangling.lean
View file

@ -40,9 +40,10 @@ String.mangleAux s.length s.mkIterator ""
private def Name.mangleAux (pre : String) : Name → String
| Name.anonymous := pre
| (Name.mkString p s) :=
let r := Name.mangleAux p in
let m := String.mangle s in
r ++ "_s" ++ toString m.length ++ "_" ++ m
match p with
| Name.anonymous := m
| _ := (Name.mangleAux p) ++ "_" ++ m
| (Name.mkNumeral p n) :=
let r := Name.mangleAux p in
r ++ "_" ++ toString n ++ "_"