aeneas icon indicating copy to clipboard operation
aeneas copied to clipboard

Published 20 hours ago • verified publisher icon AeneasVerif

Implement a congruence closure tactic

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

I'm using simp_all a lot to do what would be given by a "congruence closure" tactic, and it would be good to have such a tactic in our toolbox. There seems to exists WIP on the topic, I'm not sure how mature they are. See this for instance.

sonmarcho avatar Aug 20 '24 13:08 sonmarcho