Trait ExecSpecSetEmpty 

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

Traits for Set methods Spec for executable version of Set::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<K: DeepView + Hash + Eq> ExecSpecSetEmpty for HashSet<K>

Impls for executable versions of Map methods

exec fn exec_empty() -> res : Self

ensures

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

Implementors