Trait ExecSpecMapIndex 

pub trait ExecSpecMapIndex<'a>: Sized + DeepView<V = Map<<Self::Key as DeepView>::V, <Self::Value as DeepView>::V>> {
    type Key: DeepView;
    type Value: DeepView;

    // Required method
    exec fn exec_index(self, key: Self::Key) -> Self::Value;
}

Spec for executable version of Map indexing.

Required Associated Types

type Key: DeepView

type Value: DeepView

Required Methods

exec fn exec_index(self, key: Self::Key) -> Self::Value

requires

self.deep_view().dom().contains(key.deep_view()),

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, V: DeepView> ExecSpecMapIndex<'a> for &'a HashMap<K, V>

exec fn exec_index(self, index: Self::Key) -> res : Self::Value

ensures

res.deep_view() == self.deep_view()[index.deep_view()],

type Key = K

type Value = &'a V

Implementors