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
.