pub open spec fn set_op<RA: ResourceAlgebra>(s: Set<RA>, t: RA) -> Set<RA>Expand description
{ Set::new(|v| exists |q| s.contains(q) && v == RA::op(q, t)) }The set of values such that can be created by composing an element of s with t.
pub open spec fn set_op<RA: ResourceAlgebra>(s: Set<RA>, t: RA) -> Set<RA>{ Set::new(|v| exists |q| s.contains(q) && v == RA::op(q, t)) }The set of values such that can be created by composing an element of s with t.