fix: non-atomic identifiers in antiquotation splices

This commit is contained in:
Sebastian Ullrich 2020-12-25 22:58:33 +01:00
parent 48b92a4486
commit 82497e3bcf

View file

@ -22,7 +22,7 @@ private partial def floatOutAntiquotTerms : Syntax → StateT (Syntax → TermEl
| stx@(Syntax.node k args) => do
if isAntiquot stx && !isEscapedAntiquot stx then
let e := getAntiquotTerm stx
if !e.isIdent then
if !e.isIdent || !e.getId.isAtomic then
return ← withFreshMacroScope do
let a ← `(a)
modify (fun cont stx => (`(let $a:ident := $e; $stx) : TermElabM _))