lean4-metaprogramming-book
lean4-metaprogramming-book copied to clipboard
chapter 9 <;>
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
).