Function vstd::pcm::set_op

source · 
pub open spec fn set_op<P: PCM>(s: Set<P>, t: P) -> Set<P>
Expand description
{ Set::new(|v| exists |q| s.contains(q) && v == P::op(q, t)) }