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

refactor: simplify quoteSyntax

Browse source
This commit is contained in:
Sebastian Ullrich 2020-01-15 17:47:08 +01:00
parent b14c7cb69b
commit b1a59bb1cf
1 changed files with 1 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Lean/Elab/Quotation.lean
View file

@ -108,10 +108,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
let val := quote val;
-- `scp` is bound in stxQuot.expand
val ← `(addMacroScope $val scp);
let args := quote preresolved;
-- TODO: simplify quotations when we're no longer limited by name resolution in the old frontend
`(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) $val $args)
`(Syntax.ident none (String.toSubstring $(quote (toString rawVal))) (addMacroScope $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k args) =>
if isAntiquot stx then