diff --git a/tests/lean/run/beginEndAsMacro.lean b/tests/lean/run/beginEndAsMacro.lean new file mode 100644 index 0000000000..078b9f9922 --- /dev/null +++ b/tests/lean/run/beginEndAsMacro.lean @@ -0,0 +1,17 @@ +syntax[beginEndKind] "begin " (sepBy (allowTrailingSep := true) tactic ", ") "end" : term + +open Lean in +@[macro beginEndKind] def expandBeginEnd : Lean.Macro := fun stx => + match_syntax stx with + | `(begin $ts* end) => do + let ts := ts.getSepElems.map fun t => mkNullNode #[t, mkNullNode] + let tseq := mkNode `Lean.Parser.Tactic.tacticSeqBracketed #[mkAtomFrom stx "{", mkNullNode ts, mkAtomFrom stx[2] "}"] + `(by $tseq:tacticSeqBracketed) + | _ => Macro.throwUnsupported + +theorem ex1 (x : Nat) : x + 0 = 0 + x := + begin + rw Nat.zeroAdd, + rw Nat.addZero, + rfl + end