compatibility with Coq PR 11906

uwplse / verdi-raft

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

BSD 2-Clause "Simplified" License

183 stars 19 forks source link

compatibility with Coq PR 11906 #83

Closed fajb closed 4 years ago

fajb commented 4 years ago

Coq PR #11906 extends lia with support for boolean operators. This has the consequence that intuition is able to perform some boolean reasoning e.g. true = false -> 0 = 1. The PR replaces a call to intuition by intuition idtac.