From c005a9375a636bbed2acaf2c081c972cc2fa8dea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Oct 2020 16:50:59 -0700 Subject: [PATCH] chore: remove workarounds --- tests/lean/run/strInterpolation.lean | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/tests/lean/run/strInterpolation.lean b/tests/lean/run/strInterpolation.lean index 33508cdf69..8b0e4bd14d 100644 --- a/tests/lean/run/strInterpolation.lean +++ b/tests/lean/run/strInterpolation.lean @@ -100,11 +100,10 @@ match isLit? Parser.strInterpolantStrLitKind stx with def expandStrInterpolantChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := chunks.iterateM Syntax.missing fun i elem result => do - let elem ← (match elem.isStrInterpolantStrLit? with + let elem ← match elem.isStrInterpolantStrLit? with | none => mkElem elem - | some str => mkElem (mkStxStrLit str)) - -- TODO: remove `(` after we write new elabDo - (if i.val == 0 then pure elem else mkAppend result elem) + | some str => mkElem (mkStxStrLit str) + if i.val == 0 then pure elem else mkAppend result elem end Lean.Syntax