Function vstd::std_specs::hash::ex_hash_map_insert

source ·

pub exec fn ex_hash_map_insert<Key, Value, S>(
    m: &mut HashMap<Key, Value, S>,
    k: Key,
    v: Value
) -> result : Option<Value>where
    Key: Eq + Hash,
    S: BuildHasher,

Expand description

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& m@ == old(m)@.insert(k, v)
        &&& match result {
            Some(v) => old(m)@.contains_key(k) && v == old(m)[k],
            None => !old(m)@.contains_key(k),
        }

    },