vstd::std_specs::hash

Function hash_map_deep_view_impl

Source 
pub open spec fn hash_map_deep_view_impl<Key: DeepView, Value: DeepView, S>(
    m: HashMap<Key, Value, S>,
) -> Map<Key::V, Value::V>
Expand description
{
    Map::new(
        |k: Key::V| {
            exists |orig_k: Key| (
                #[trigger] m@.contains_key(orig_k) && k == orig_k.deep_view()
            )
        },
        |dk: Key::V| {
            let k = choose |k: Key| m@.contains_key(k) && #[trigger] k.deep_view() == dk;
            m@[k].deep_view()
        },
    )
}

The actual definition of HashMap::deep_view.

This is a separate function since it introduces a lot of quantifiers and revealing an opaque trait method is not supported. In most cases, it’s easier to use one of the lemmas below instead of revealing this function directly.