Module imap 

Macros

assert_imaps_equal

Prove two maps map1 and map2 are equal by proving that their values are equal at each key.

imap

Create a map using syntax like imap![key1 => val1, key2 => val, ...].

Structs

IMap

IMap<K, V> is an abstract map type for specifications.

Functions

axiom_imap_index_decreases_finite

axiom_imap_index_decreases_infinite

group_imap_lemmas

lemma_imap_empty

lemma_imap_ext_equal

lemma_imap_ext_equal_deep

lemma_imap_insert_different

lemma_imap_insert_domain

lemma_imap_insert_same

lemma_imap_remove_different

lemma_imap_remove_domain