axiom_btree_map_deepview_borrow

vstd::std_specs::btree

Function axiom_btree_map_deepview_borrow 

Source 
pub broadcast proof fn axiom_btree_map_deepview_borrow<K: DeepView + Borrow<Q>, V: DeepView, Q: View<V = <K as DeepView>::V> + Eq + ?Sized>(
    m: BTreeMap<K, V>,
    k: &Q,
)
Expand description
requires
key_obeys_cmp_spec::<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.