Function vstd::std_specs::hash::axiom_box_key_removed

pub broadcast proof fn axiom_box_key_removed<Q, Value>(
    old_m: Map<Box<Q>, Value>,
    new_m: Map<Box<Q>, Value>,
    q: &Q
)

Expand description

ensures

#[trigger] borrowed_key_removed::<Box<Q>, Value, Q>(old_m, new_m, q)
    <==> new_m == old_m.remove(Box::new(*q)),

Function vstd::std_specs::hash::axiom_box_key_removedCopy item path