Struct Multiset 

pub struct Multiset<V: DafnyTypeEq> {
    pub data: HashMap<V, DafnyInt>,
    pub size: DafnyInt,
}

Fields

data: HashMap<V, DafnyInt>

size: DafnyInt

Implementations

impl<V: DafnyTypeEq> Multiset<V>

pub fn new_empty() -> Multiset<V>

pub fn get_total(map: &HashMap<V, DafnyInt>) -> DafnyInt

pub fn from_hashmap_owned(map: HashMap<V, DafnyInt>) -> Multiset<V>

pub fn from_hashmap(map: &HashMap<V, DafnyInt>) -> Multiset<V>

pub fn from_array(data: &Vec<V>) -> Multiset<V>

pub fn from_iterator<I>(data: I) -> Multiset<V>

where I: Iterator<Item = V>,

pub fn from_set(set: &Set<V>) -> Multiset<V>

pub fn cardinality_usize(&self) -> SizeT

pub fn cardinality(&self) -> DafnyInt

pub fn contains(&self, value: &V) -> bool

pub fn get(&self, value: &V) -> DafnyInt

pub fn update_count(&self, value: &V, new_count: &DafnyInt) -> Multiset<V>

pub fn merge(&self, other: &Multiset<V>) -> Multiset<V>

pub fn intersect(&self, other: &Multiset<V>) -> Multiset<V>

pub fn subtract(&self, other: &Multiset<V>) -> Multiset<V>

pub fn disjoint(&self, other: &Multiset<V>) -> bool

pub fn as_dafny_multiset(&self) -> Multiset<V>

pub fn peek(&self) -> V

pub fn iter_raw(&self) -> Iter<'_, V, DafnyInt>

pub fn iter(&self) -> impl Iterator<Item = V> + '_

impl<U: DafnyTypeEq> Multiset<U>

pub fn coerce<V: DafnyTypeEq>( f: Rc<impl Fn(U) -> V>, ) -> Rc<impl Fn(Multiset<U>) -> Multiset<V>>

Trait Implementations

impl<V: Clone + DafnyTypeEq> Clone for Multiset<V>

fn clone(&self) -> Multiset<V>

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl<V: DafnyTypeEq> DafnyPrint for Multiset<V>

fn fmt_print(&self, f: &mut Formatter<'_>, in_seq: bool) -> Result

fn is_char() -> bool

impl<V> Debug for Multiset<V>

where V: DafnyTypeEq,

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<T> Default for Multiset<T>

where T: DafnyTypeEq,

fn default() -> Self

Returns the “default value” for a type.

impl<V: DafnyTypeEq> Hash for Multiset<V>

fn hash<H: Hasher>(&self, state: &mut H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl<T: DafnyTypeEq> NontrivialDefault for Multiset<T>

fn nontrivial_default() -> Self

impl<V: DafnyTypeEq> PartialEq for Multiset<V>

fn eq(&self, other: &Multiset<V>) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl<V: DafnyTypeEq> PartialOrd for Multiset<V>

fn partial_cmp(&self, other: &Multiset<V>) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl<V: DafnyTypeEq> Eq for Multiset<V>