kdrag.theories.set.Quot

kdrag.theories.set.Quot(dom: SortRef, eqrel) → QuantifierRef

Quotient space under equivalence relation eqrel. A set of sets of A. The set of equivalence classes https://en.wikipedia.org/wiki/Equivalence_class

>>> x = smt.Int("x")
>>> l = kd.Lemma((smt.IntSort() // (lambda a,b: a % 3 == b % 3))[EClass(x, lambda a,b: a % 3 == b % 3)])
>>> l.simp().exists(x).auto()
Nothing to do. Hooray!
>>> _ = l.qed()

Parameters:

dom (SortRef)

Return type:

QuantifierRef