Module 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 that has a Map<K, V> as its specification type.

Functions

axiom_map_ext_equal

axiom_map_ext_equal_deep

axiom_map_index_decreases

axiom_map_insert_different

axiom_map_remove_different

group_map_lemmas

lemma_map_empty

lemma_map_insert_domain

lemma_map_insert_same

lemma_map_new_domain

lemma_map_new_index

lemma_map_remove_domain