Skip to main content

FiniteSet

structure FiniteSet[T] {
    underlying_set: Set[T]
} constraint {
    underlying_set.is_finite
}

A finite set is a Set bundled with a finiteness proof.

GitHub

as_set​

define as_set(self) -> Set[T] {
    self.underlying_set
}

Access the underlying set.

cardinality_at_most​

define cardinality_at_most(self, n: Nat) -> Bool {
    self.underlying_set.cardinality_at_most(n)
}

Cardinality helper lifted from sets.

cardinality_is​

define cardinality_is(self, n: Nat) -> Bool {
    self.underlying_set.cardinality_is(n)
}

True if the cardinality equals n.

contains​

define contains(self, x: T) -> Bool {
    self.underlying_set.contains(x)
}

Membership predicate.

difference​

define difference(self, other: FiniteSet[T]) -> FiniteSet[T] {
    FiniteSet.new(self.underlying_set.difference(other.underlying_set))
}

Difference of finite sets.

empty​

let empty: FiniteSet[T] = FiniteSet.new(Set[T].empty_set)

The empty finite set.

insert​

define insert(self, item: T) -> FiniteSet[T] {
    FiniteSet.new(self.underlying_set.insert(item))
}

Insert preserves finiteness.

intersection​

define intersection(self, other: FiniteSet[T]) -> FiniteSet[T] {
    FiniteSet.new(self.underlying_set.intersection(other.underlying_set))
}

Intersection of finite sets.

is_disjoint​

define is_disjoint(self, other: FiniteSet[T]) -> Bool {
    self.underlying_set.is_disjoint(other.underlying_set)
}

Disjointness predicate.

is_empty​

define is_empty(self) -> Bool {
    self.underlying_set.is_empty
}

Empty predicate.

remove​

define remove(self, item: T) -> FiniteSet[T] {
    FiniteSet.new(self.underlying_set.remove(item))
}

Remove preserves finiteness.

subset_eq​

define subset_eq(self, other: FiniteSet[T]) -> Bool {
    self.underlying_set.subset(other.underlying_set)
}

Subset relation lifted from sets.

superset_eq​

define superset_eq(self, other: FiniteSet[T]) -> Bool {
    self.underlying_set.superset(other.underlying_set)
}

Superset relation lifted from sets.

underlying_set​

FiniteSet.underlying_set: FiniteSet[T] -> Set[T]

The underlying set.

union​

define union(self, other: FiniteSet[T]) -> FiniteSet[T] {
    FiniteSet.new(self.underlying_set.union(other.underlying_set))
}

Union of finite sets.