Function vstd::std_specs::hash::ex_hash_map_remove

source ·

pub exec fn ex_hash_map_remove<Key, Value, S, Q>(
    m: &mut HashMap<Key, Value, S>,
    k: &Q
) -> result : Option<Value>where
    Key: Borrow<Q> + Hash + Eq,
    Q: Hash + Eq + ?Sized,
    S: BuildHasher,

Expand description

ensures

obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> {
        &&& borrowed_key_removed(old(m)@, m@, k)
        &&& match result {
            Some(v) => maps_borrowed_key_to_value(old(m)@, k, v),
            None => !contains_borrowed_key(old(m)@, k),
        }

    },