Function vstd::map::axiom_map_insert_same

pub broadcast proof fn axiom_map_insert_same<K, V>(m: Map<K, V>, key: K, value: V)

Expand description

ensures

#[trigger] m.insert(key, value)[key] == value,

Inserting value at key in m results in a map that maps key to value

Function vstd::map::axiom_map_insert_sameCopy item path