Module EquivalenceRelation

Provides predicates and types for working with (partial) equivalence relations over arbitrary types.

The module is parameterised by a type T and a binary base relation eq over T. A (partial) equivalence relation is computed from the given base relation eq as the symmetric and transitive closure of eq. If eq is reflexive, then this defines an equivalence relation on T.

The getEquivalenceClass predicate gets the equivalence class, if any, induced by the symmetric and transitive closure of eq, for the given T element.