Module vstd::map

Macros

• assert_maps_equal
  Prove two maps map1 and map2 are equal by proving that their values are equal at each key.
• map
  Create a map using syntax like map![key1 => val1, key2 => val, ...].

Structs

• Map
  Map<K, V> is an abstract map type for specifications. To use a “map” in compiled code, use an exec type like HashMap (TODO) that has a Map<K, V> as its specification type.

Functions

• axiom_map_empty
• axiom_map_ext_equal
• axiom_map_ext_equal_deep
• axiom_map_index_decreases_finite
• axiom_map_index_decreases_infinite
• axiom_map_insert_different
• axiom_map_insert_domain
• axiom_map_insert_same
• axiom_map_remove_different
• axiom_map_remove_domain
• group_map_axioms