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

chore: remove addMacroScopeExt

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-23 12:08:20 -08:00
parent 0a59e53265
commit 0228f9c9b7
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Init/LeanInit.lean
View file

@ -256,9 +256,6 @@ We use two delimiters for improving `hasMacroScopes` performance.
private def mkMacroScopeName (mainModule : Name) (n : Name) : Name :=
mkNameStr (mkNameStr n "_@" ++ mainModule) "_hyg"
def addMacroScopeExt (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
mkNameNum (mkMacroScopeName mainModule n) scp
def addMacroScope (mainModule : Name) (n : Name) (scp : MacroScope) : Name :=
mkNameNum (mkMacroScopeName mainModule n) scp