Trait ExecSpecSeqEmpty 

pub trait ExecSpecSeqEmpty: Sized {
    // Required method
    exec fn exec_empty() -> Self;
}

Spec for executable version of Seq::empty.

Required Methods

exec fn exec_empty() -> Self

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<T: DeepView> ExecSpecSeqEmpty for Vec<T>

exec fn exec_empty() -> res : Self

ensures

res.deep_view() =~= Seq::empty(),

Implementors