Struct creusot_contracts::logic::Set

pub struct Set<T: ?Sized>(/* private fields */);

A (possibly infinite) set type.

Implementations

impl<T: ?Sized> Set<T>

pub const EMPTY: Self = _

The empty set.

pub fn contains(self, e: T) -> bool

Returns true if e is in the set.

logic

Self::mem(e, self)

pub fn insert(self, e: T) -> Self

Returns a new set, where e has been added if it was not present.

logic

Self::add(e, self)

pub fn is_empty(self) -> bool

Returns true if the set contains no elements.

logic

pub fn remove(self, a: T) -> Self

Returns a new set, where e is no longer present.

logic

Self::rem(a, self)

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

Returns a new set, which is the union of self and other.

An element is in the result if it is in self or if it is in other.

logic