Function vstd::std_specs::hash::axiom_maps_deref_key_to_value

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