Function vstd::std_specs::hash::axiom_maps_box_key_to_value

source ·

pub broadcast proof fn axiom_maps_box_key_to_value<Q, Value>(
    m: Map<Box<Q>, Value>,
    q: &Q,
    v: Value
)

Expand description

ensures

#[trigger] maps_borrowed_key_to_value::<Box<Q>, Value, Q>(m, q, v)
    <==> {
        let k = Box::new(*q);
        &&& m.contains_key(k)
        &&& m[k] == v

    },