Make inequality chains work for simple algebraic structures and equality - Githubissues

impermeable / coq-waterproof

GNU Lesser General Public License v3.0

29 stars 9 forks source link

Make inequality chains work for simple algebraic structures and equality #8

Closed jim-portegies closed 1 year ago

jim-portegies commented 1 year ago

Create a new hints database waterproof_algebra
Add f_equal, f_equal2, and the congruence tactic to this hint database
Split conjunctions for inequality chains.