pub trait ExecSpecSeqEmpty: Sized {
// Required method
exec fn exec_empty() -> Self;
}Expand description
Spec for executable version of Seq::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<T: DeepView> ExecSpecSeqEmpty for Vec<T>
impl<T: DeepView> ExecSpecSeqEmpty for Vec<T>
Source§exec fn exec_empty() -> res : Self
exec fn exec_empty() -> res : Self
ensures
res.deep_view() =~= Seq::empty(),