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 (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