Trait ExecSpecSetContains 

pub trait ExecSpecSetContains<'a>: Sized + DeepView {
    type Elem: DeepView;

    // Required method
    exec fn exec_contains(self, a: Self::Elem) -> bool;
}

Spec for executable version of Set::contains.

Required Associated Types

type Elem: DeepView

Required Methods

exec fn exec_contains(self, a: Self::Elem) -> bool

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl<'a, K: DeepView + Hash + Eq> ExecSpecSetContains<'a> for &'a HashSet<K>

exec fn exec_contains(self, a: Self::Elem) -> res : bool

ensures

res == self.deep_view().contains(a.deep_view()),

type Elem = K

Implementors