Struct Multiset 

pub struct Multiset<V> { /* private fields */ }

Multiset<V> is an abstract multiset type for specifications.

Multiset<V> can be encoded as a (total) map from elements to natural numbers, where the number of nonzero entries is finite.

Multisets can be constructed in a few different ways:

• [Multiset::empty] constructs an empty multiset.
• [Multiset::singleton] constructs a multiset that contains a single element with multiplicity 1.
• [Multiset::from_map] constructs a multiset from a map of elements to multiplicities.
• By manipulating existings multisets with [Multiset::add], [Multiset::insert], [Multiset::sub], [Multiset::remove], [Multiset::update], or [Multiset::filter].
• TODO: multiset! constructor macro, multiset from set, from map, etc.

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