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

@@ -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