kdrag.theories.algebra.filter

Functions

Filter(T)

A sort generic filter over sets of type T.

Classes

FilterMod(T)

A module encapsulating filter theory over sets of type T.

kdrag.theories.algebra.filter.Filter(T: SortRef)

A sort generic filter over sets of type T.

>>> Filter(smt.RealSort())
Filter_Real

Parameters:

T (SortRef)

class kdrag.theories.algebra.filter.FilterMod(T: SortRef)

Bases: object

A module encapsulating filter theory over sets of type T.

>>> FilterMod(smt.RealSort()).filter_full
|= ForAll(F, Implies(wf(F), sets(F)[K(Real, True)]))

Parameters:

T (SortRef)