pub trait ExecSpecSetIntersect<'a, Out: Sized + DeepView>:
Sized
+ DeepView
+ ToOwned<Out> {
// Required method
exec fn exec_intersect(self, s2: Self) -> Out;
}Expand description
Spec for executable version of Set::intersect.
Required Methods§
Sourceexec fn exec_intersect(self, s2: Self) -> Out
exec fn exec_intersect(self, s2: Self) -> Out
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety".
Implementations on Foreign Types§
Source§impl<'a, K> ExecSpecSetIntersect<'a, HashSet<K>> for &'a HashSet<K>
impl<'a, K> ExecSpecSetIntersect<'a, HashSet<K>> for &'a HashSet<K>
Source§exec fn exec_intersect(self, s2: Self) -> res : HashSet<K>
exec fn exec_intersect(self, s2: Self) -> res : HashSet<K>
ensures
res.deep_view() =~= self.deep_view().intersect(s2.deep_view()),