Trait ExecSpecMapEmpty 

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

Traits for Map methods Spec for executable version of Map::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, V: DeepView> ExecSpecMapEmpty for HashMap<K, V>

Impls for executable versions of Map methods

exec fn exec_empty() -> res : Self

ensures

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

Implementors