lean4-metaprogramming-book icon indicating copy to clipboard operation
lean4-metaprogramming-book copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chapter 9 <;>

Open fpvandoorn opened this issue 1 year ago • 0 comments
trafficstars

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).

fpvandoorn avatar Dec 07 '23 23:12 fpvandoorn