pub trait ExecSpecSetEmpty: Sized {
// Required method
exec fn exec_empty() -> Self;
}Expand description
Traits for Set methods
Spec for executable version of Set::empty.
Required Methods§
Sourceexec fn exec_empty() -> Self
exec fn exec_empty() -> Self
Dyn Compatibility§
This trait is not dyn compatible.
In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.
Implementations on Foreign Types§
Source§impl<K: DeepView + Hash + Eq> ExecSpecSetEmpty for HashSet<K>
Impls for executable versions of Map methods
impl<K: DeepView + Hash + Eq> ExecSpecSetEmpty for HashSet<K>
Impls for executable versions of Map methods
Source§exec fn exec_empty() -> res : Self
exec fn exec_empty() -> res : Self
ensures
res.deep_view() =~= Set::empty(),