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