Zulip Chat Archive
Stream: lean4
Topic: Incorrect Name Mangling
Naveen (Jun 21 2021 at 16:27):
Hi,
It seems, the name mangler only handles utf-16 unicode characters. See here. This has caused to output bad name during building of mathlib4.
#eval "𝒫".mangle
-- outputs `_u*4ab`
Wojciech Nawrocki (Jun 21 2021 at 18:09):
https://github.com/leanprover/lean4/pull/539
Last updated: Dec 20 2023 at 11:08 UTC