Struct Class

pub struct Class(/* private fields */);

A class of hereditarily finite sets.

We define this as an arbitrary iterator over Set without duplicate entries. This allows for many important constructions, such as the universal class or for classes from a predicate.

Note that since classes represent potentially infinite collections, it’s possible for a piece of code to hang. For instance,

Class::pred(|_| false).into_iter().next();

will run forever, unsucessfully testing the predicate on each set. This limitation means that certain relations, like membership or subsets, cannot be determined in general.

Invariants

Every two elements outputted by a Class must be distinct. Unsafe code can perform optimizations contingent on this.

Implementations

impl Class

pub unsafe fn new_unchecked<I: Iterator<Item = Set> + 'static>(iter: I) -> Self

Initializes a new class from an iterator.

Safety

You must guarantee that any two sets returned by the iterator are distinct.

pub fn new<I: Iterator<Item = Set> + 'static>(iter: I) -> Self

Initializes a new class from an iterator. This iterator is deduplicated via Dedup.

pub fn contains(self, set: &Set) -> bool

Determines whether a class contains a given set.

This will hang indefinitely if the class is infinite and the set is not contained in it.

pub fn empty() -> Self

The empty class Ø.

pub fn univ() -> Self

The universal class, defined via Univ.

pub fn nat() -> Self

The class of naturals ℕ, defined via Nat.

pub fn zermelo() -> Self

The class of Zermelo naturals ℕ, defined via Zermelo.

pub fn neumann() -> Self

The von Neumann hierarchy up to V_ω, defined via Neumann.

pub fn select<P: FnMut(&Set) -> bool + 'static>(self, pred: P) -> Self

Class specification.

pub fn pred<P: FnMut(&Set) -> bool + 'static>(pred: P) -> Self

Initializes a new class from a predicate.

This iterates over the universal class and selects the elements satisfying the predicate. If they ever run out, the iterator will continue searching forever.

pub fn union_iter<I: Iterator<Item = Self> + 'static>(iter: I) -> Self

Class union over an iterator.

This internally uses Interleave to get the elements out of each set.

pub fn union_vec(vec: Vec<Self>) -> Self

Class union over a vector.

This internally uses Interleave to get the elements out of each set.

pub fn union(self, other: Self) -> Self

Class union.

This internally uses Interleave to get the elements out of each set.

pub fn prod(self, other: Self) -> Self

Cartesian product of classes.

This internally uses Product to get the elements out of each set.

pub fn replace<F: FnMut(Set) -> Set + 'static>(self, func: F) -> Self

Replaces the elements in a class by applying a function.

pub unsafe fn replace_unchecked<F: FnMut(Set) -> Set + 'static>( self, func: F, ) -> Self

Replaces the elements in a class by applying a function. Does not check that the outputs are all distinct.

Safety

You must guarantee that the function does not yield the same output for two distinct elements of the class.

pub fn choose(self) -> Option<Set>

Chooses an arbitrary element from a non-empty class, by calling next.

Trait Implementations

impl Default for Class

fn default() -> Self

Returns the “default value” for a type.

impl From<Set> for Class

fn from(value: Set) -> Self

Converts to this type from the input type.

impl IntoIterator for Class

type Item = <Box<dyn Iterator<Item = Set>> as IntoIterator>::Item

The type of the elements being iterated over.

type IntoIter = <Box<dyn Iterator<Item = Set>> as IntoIterator>::IntoIter

Which kind of iterator are we turning this into?

fn into_iter(self) -> Self::IntoIter

Creates an iterator from a value.