Struct Map 

pub struct Map<K, V>
where
    K: DafnyTypeEq,
    V: DafnyType,
{ /* private fields */ }

Implementations

impl<K: DafnyTypeEq, V: DafnyType> Map<K, V>

pub fn new_empty() -> Map<K, V>

pub fn from_array(values: &Vec<(K, V)>) -> Map<K, V>

pub fn from_iterator<I>(data: I) -> Map<K, V>

where I: Iterator<Item = (K, V)>,

pub fn from_hashmap_owned(values: HashMap<K, V>) -> Map<K, V>

pub fn to_hashmap_owned<K2, V2>( &self, converter_k: fn(&K) -> K2, converter_v: fn(&V) -> V2, ) -> HashMap<K2, V2>

where K2: Eq + Hash, V2: Clone,

pub fn cardinality_usize(&self) -> usize

pub fn cardinality(&self) -> DafnyInt

pub fn contains(&self, key: &K) -> bool

pub fn get_or_none(&self, key: &K) -> Option<V>

pub fn get(&self, key: &K) -> V

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

pub fn subtract(&self, keys: &Set<K>) -> Self

pub fn from_hashmap<K2, V2>( map: &HashMap<K2, V2>, converter_k: fn(&K2) -> K, converter_v: fn(&V2) -> V, ) -> Map<K, V>

where K: DafnyTypeEq, V: DafnyTypeEq, K2: Eq + Hash, V2: Clone,

pub fn keys(&self) -> Set<K>

pub fn update_index(&self, index: &K, value: &V) -> Self

pub fn update_index_owned(&self, index: K, value: V) -> Self

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

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

impl<K: DafnyTypeEq, V: DafnyTypeEq> Map<K, V>

pub fn values(&self) -> Set<V>

pub fn items(&self) -> Set<(K, V)>

impl<K: DafnyTypeEq> Map<K, DafnyInt>

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

impl<K: DafnyTypeEq, U: DafnyTypeEq> Map<K, U>

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

Trait Implementations

impl<K, V> Clone for Map<K, V>

where K: DafnyTypeEq + Clone, V: DafnyType + Clone,

fn clone(&self) -> Map<K, V>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<K, V> DafnyPrint for Map<K, V>

where K: DafnyTypeEq, V: DafnyType,

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

fn is_char() -> bool

impl<K, V> Debug for Map<K, V>

where K: DafnyTypeEq, V: DafnyTypeEq,

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

Formats the value using the given formatter.

impl<K: DafnyTypeEq, V: DafnyType> Default for Map<K, V>

fn default() -> Self

Returns the “default value” for a type.

impl<K: DafnyTypeEq, V: DafnyType> Hash for Map<K, 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<K: DafnyTypeEq, V: DafnyType> NontrivialDefault for Map<K, V>

fn nontrivial_default() -> Self

impl<K, V> PartialEq for Map<K, V>

where K: DafnyTypeEq, V: DafnyTypeEq,

fn eq(&self, other: &Map<K, 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<K: DafnyTypeEq, V: DafnyTypeEq> Eq for Map<K, V>