Struct vstd::map::Map

An empty map.

Gives a Map<K, V> whose domain contains every key, and maps each key to the value given by fv.

Gives a Map<K, V> whose domain is given by the boolean predicate on keys fk, and maps each key to the value given by fv.

The domain of the map as a set.

self.dom().contains(key),

Gets the value that the given key key maps to. For keys not in the domain, the result is meaningless and arbitrary.

self.dom().contains(key),

[] operator, synonymous with index

Inserts the given (key, value) pair into the map.

If the key is already present from the map, then its existing value is overwritten by the new value.

Removes the given key and its associated value from the map.

If the key is already absent from the map, then the map is left unchanged.

Returns the number of key-value pairs in the map

DEPRECATED: use =~= or =~~= instead. Returns true if the two maps are pointwise equal, i.e., they have the same domains and the corresponding values are equal for each key. This is equivalent to the maps being actually equal by axiom_map_ext_equal.

To prove that two maps are equal via extensionality, it may be easier to use the general-purpose =~= or =~~= or to use the assert_maps_equal! macro, rather than using .ext_equal directly.

old(self).dom().contains(key),

*self == Map::remove(*old(self), key),

v == old(self)[key],

todo fill in documentation

Is true if called by a “full” map, i.e., a map containing every element of type A.

Is true if called by an “empty” map, i.e., a map containing no elements and has length 0

Returns true if the key k is in the domain of self.

Returns true if the value v is in the range of self.

Returns the set of values in the map.

Example

assert(
   map![1 => 10, 2 => 11].values() =~= set![10, 11]
);

Returns true if the key k is in the domain of self, and it maps to the value v.

Returns true if m1 is contained in m2, i.e., the domain of m1 is a subset of the domain of m2, and they agree on all values in m1.

Example

assert(
   map![1 => 10, 2 => 11].le(map![1 => 10, 2 => 11, 3 => 12])
);

Deprecated synonym for submap_of

Gives the union of two maps, defined as:

• The domain is the union of the two input maps.
• For a given key in both input maps, it maps to the same value that it maps to in the right map (m2).
• For any other key in either input map (but not both), it maps to the same value as it does in that map.

Example

assert(
   map![1 => 10, 2 => 11].union_prefer_right(map![1 => 20, 3 => 13])
   =~= map![1 => 20, 2 => 11, 3 => 13]);

Removes the given keys and their associated values from the map.

Ignores any key in keys which is not in the domain of self.

Example

assert(
   map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
   =~= map![1 => 10]);

Complement to remove_keys. Restricts the map to (key, value) pairs for keys that are in the given set; that is, it removes any keys not in the set.

Example

assert(
   map![1 => 10, 2 => 11, 3 => 12].remove_keys(set!{2, 3, 4})
   =~= map![2 => 11, 3 => 12]);

Returns true if and only if the given key maps to the same value or does not exist in self and m2.

Returns true if the two given maps agree on all keys that their domains share

Map a function f over all (k, v) pairs in self.

Map a function f over the values in self.

Returns true if and only if a map is injective

Swaps map keys and values. Values are not required to be unique; no promises on which key is chosen on the intersection.

self.dom().contains(key),

self.dom().finite(),

self.dom().len() == 1 + self.remove(key).dom().len(),

Removing a key from a map that previously contained that key decreases the map’s length by one

self.remove(key).dom() == self.dom().remove(key),

The domain of a map after removing a key is equivalent to removing the key from the domain of the original map.

forall |k: K| #[trigger] keys.contains(k) ==> self.contains_key(k),

keys.finite(),

self.dom().finite(),

self.remove_keys(keys).dom().len() == self.dom().len() - keys.len(),

Removing a set of n keys from a map that previously contained all n keys results in a domain of size n less than the original domain.

self.invert().is_injective(),

The function invert results in an injective map

Returns true if a map is monotonic – that is, if the mapping between ordered sets preserves the regular <= ordering on integers.

Returns true if and only if a map is monotonic, only considering keys greater than or equal to start

Returns the argument unchanged.

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.