vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
302 stars 52 forks source link

remove the commutative bit, equations still treated as commutative #612

Closed MichaelRawson closed 2 months ago

MichaelRawson commented 2 months ago

As discussed internally, commutative terms don't actually exist apart from equations. Remove the commutative bit and code that relies on it, instead checking for equations where it makes sense to do so.

While we're at it, also remove some dead code, tag #157.