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