QuotientRelation

structure QuotientRelation[T] {
    rel: (T, T) -> Bool
} constraint {
    is_equivalence(rel)
}

A relation together with the fact that it is an equivalence relation.

GitHub

---

rel

QuotientRelation.rel: (QuotientRelation[T], T, T) -> Bool

The relation whose equivalence classes form quotient elements.