Function vstd::storage_protocol::set_op

source · 
pub open spec fn set_op<K, V, P: Protocol<K, V>>(
    s: Set<(P, Map<K, V>)>,
    t: P
) -> Set<(P, Map<K, V>)>
Expand description
{
    Set::new(|v: (P, Map<K, V>)| {
        exists |q| s.contains((q, v.1)) && v.0 == #[trigger] P::op(q, t)
    })
}