max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: simplify begin..end macro

Browse source 
The method `getRef` returns the whole term being expanded.
@Kha The method was originially added for reporting error messages.
So, the name is counterintuitive.
This commit is contained in:
Leonardo de Moura 2020-11-24 11:04:06 -08:00
parent 3eaa4518a0
commit fa04f46d55
1 changed files with 7 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
doc/tactics.md
View file

@ -252,18 +252,14 @@ If you love Lean 3 `begin ... end` tactic blocks and commas, you can define this
in Lean 4 using macros in a few lines of code.
```lean
syntax[beginEndKind] "begin " sepByT(tactic, ", ") "end" : term
open Lean in
@[macro beginEndKind] def expandBeginEnd : 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
macro "begin " ts:sepByT(tactic, ", ") "end" : term => do
let stx ← getRef
let ts := ts.getSepArgs.map (mkNullNode #[·, mkNullNode])
let tseq := mkNode `Lean.Parser.Tactic.tacticSeqBracketed #[
mkAtomFrom stx "{", mkNullNode ts, mkAtomFrom stx[2] "}"
]
`(by $tseq:tacticSeqBracketed)
theorem ex (x : Nat) : x + 0 = 0 + x :=
begin