fix: antiquotation splices early in bootstrapping

This commit is contained in:
Sebastian Ullrich 2022-03-21 17:43:53 +01:00
parent 3d9e587862
commit faedfbe651

View file

@ -140,7 +140,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
`(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))
else pure arr
let arr ← bindLets arr
args := args.append arr
args := args.append (appendName := appendName) arr
else do
let arg ← quoteSyntax arg
args := args.push arg