Function vstd::std_specs::hash::ex_hash_contains_key

source ·
pub exec fn ex_hash_contains_key<Key, Value, S, Q>(
    m: &HashMap<Key, Value, S>,
    k: &Q
) -> result : bool
where Key: Borrow<Q> + Hash + Eq, Q: Hash + Eq + ?Sized, S: BuildHasher,
Expand description
ensures
obeys_key_model::<Key>() && builds_valid_hashers::<S>()
    ==> result == contains_borrowed_key(m@, k),