Skip to main content

FiniteSet

structure FiniteSet<T> {
    contains: T -> Bool
} constraint {
    finite_constraint(contains)
}

A finite set represented as a boolean membership function. The constraint ensures that only finitely many elements are members.

GitHub

contains​

FiniteSet.contains: (FiniteSet<T>, T) -> Bool

Finite sets are defined by a membership function.

from_list​

let from_list: List<T> -> FiniteSet<T> = function(ts: List<T>) {
    FiniteSet.new(ts.contains)
}

Converts a list to a finite set.

insert​

define insert(self, item: T) -> FiniteSet<T> {
    FiniteSet.new(functional_insert(self.contains, item))
}

Adds an element to the set. If the item is already present, this is a no-op.

is_empty​

define is_empty(self) -> Bool {
    forall(x: T) {
        not self.contains(x)
    }
}

True if the set contains no elements.

remove​

define remove(self, item: T) -> FiniteSet<T> {
    FiniteSet.new(functional_remove(self.contains, item))
}

Removes an element from the set. If the item isn't present, this is a no-op.