leanprover-community / lean4-metaprogramming-book

https://leanprover-community.github.io/lean4-metaprogramming-book/
Apache License 2.0
204 stars 47 forks source link

chapter 9 <;> #119

Open fpvandoorn opened 7 months ago

fpvandoorn commented 7 months ago

The implementation (and description) of <;> is wrong: it should only apply the second tactic to goals produced by the first tactic (implementation is missing a focus).