·
24 commits
to master
since this release
This release contains the next-generation equivalence reasoner, which has been written from scratch and has the following advantages over the initial equivalence reasoner:
-
Premises may contain fixed variables and functions that are incompatible with the equivalence relation.
-
Configuration is much simpler, without any need for quotient type definitions, definitions of lifted constants, and low-level attribute applications.
-
In addition to the equivalence relation inclusions that are directly given by the user, also those that can be obtained from them by applying transitivity of the inclusion relation are taken into account.
This release also contains usage documentation, which the initial equivalence reasoner is lacking.