vstd::std_specs::hash

Function axiom_hashmap_deepview_borrow

Source 
pub broadcast proof fn axiom_hashmap_deepview_borrow<K: DeepView + Borrow<Q>, V: DeepView, Q: View<V = <K as DeepView>::V> + Hash + Eq + ?Sized>(
    m: HashMap<K, V>,
    k: &Q,
)
Expand description
requires
obeys_key_model::<K>(),
crate::relations::injective(|k: K| k.deep_view()),
ensures
#[trigger] contains_borrowed_key(m@, k) <==> m.deep_view().contains_key(k@),

Borrowing a key works the same way on deep_view as on view, if deep_view is injective; see axiom_contains_deref_key.