Function vstd::std_specs::hash::axiom_contains_box

source · 
pub broadcast proof fn axiom_contains_box<Q, Value>(m: Map<Box<Q>, Value>, k: &Q)
Expand description
ensures
#[trigger] contains_borrowed_key::<Box<Q>, Value, Q>(m, k)
    <==> m.contains_key(Box::new(*k)),