From ded043bd5381c2df3f4c2db7cf2f82f670247ea8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Nov 2020 11:53:13 -0800 Subject: [PATCH] test: old Lean3 `begin ... end` as a macro @Kha I am adding a few examples to use in the manual. This one is a bit ugly due to two issues 1- We can't easily copy the position information from one token to another. You suggested a notation in the past, but we never implemented it. In the new example, we must copy the `end` position to `}` to get the "unsolved goals" error message at the `end` token. 2- The quotation `` `(by { $ts* }) `` doesn't do what we want. The issue is that we are using `group` instead of `nodeWithAntiquot` to define `tacticSeqBracketed`. I will have to go over all parsers we have defined, and check how many other places have this problem. --- tests/lean/run/beginEndAsMacro.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 tests/lean/run/beginEndAsMacro.lean 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