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

chore: export Name.eraseMacroScopes

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-15 11:35:32 -07:00
parent 908e5f7acd
commit 54c1607b36
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/LeanInit.lean
View file

@ -334,6 +334,7 @@ private def eraseMacroScopesAux : Name → Name
| Name.num p _ _ => eraseMacroScopesAux p
| Name.anonymous => unreachable!
@[export lean_erase_macro_scopes]
def Name.eraseMacroScopes (n : Name) : Name :=
if n.hasMacroScopes then eraseMacroScopesAux n else n