Struct Set 

pub struct Set<A> { /* private fields */ }

Set<A> is a finite set type for specifications.

An object set: Set<A> is a subset of the set of all values a: A. Equivalently, it can be thought of as a boolean predicate on A.

Sets can be constructed in a few different ways:

• [Set::empty] gives an empty set
• [Set::new] constructs a set from a boolean predicate
• The set! macro, to construct small sets of a fixed size
• By manipulating an existing sequence with [Set::union], [Set::intersect], [Set::difference], [Set::complement], [Set::filter], [Set::insert], or [Set::remove].

To prove that two sequences are equal, it is usually easiest to use the extensionality operator =~=.

Set only holds finite sets, so it can be used in recursive types. For instance, a type T can contain a Set<T>.