pub trait ExecSpecMapEmpty: Sized {
// Required method
exec fn exec_empty() -> Self;
}Expand description
Traits for Map methods
Spec for executable version of Map::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, V: DeepView> ExecSpecMapEmpty for HashMap<K, V>
Impls for executable versions of Map methods
impl<K: DeepView + Hash + Eq, V: DeepView> ExecSpecMapEmpty for HashMap<K, V>
Impls for executable versions of Map methods
Source§exec fn exec_empty() -> res : Self
exec fn exec_empty() -> res : Self
ensures
res.deep_view() =~= Map::empty(),