Trait ExecSpecIndex 

pub trait ExecSpecIndex<'a>: Sized + DeepView<V = Seq<<Self::Elem as DeepView>::V>> {
    type Elem: DeepView;

    // Required method
    exec fn exec_index(self, index: usize) -> Self::Elem;
}

Spec for executable version of Seq and str indexing.

Required Associated Types

type Elem: DeepView

Required Methods

exec fn exec_index(self, index: usize) -> Self::Elem

requires

0 <= index < self.deep_view().len(),

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, T: DeepView> ExecSpecIndex<'a> for &'a [T]

exec fn exec_index(self, index: usize) -> res : Self::Elem

ensures

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

type Elem = &'a T

impl<'a> ExecSpecIndex<'a> for &'a str

exec fn exec_index(self, index: usize) -> res : Self::Elem

ensures

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

type Elem = char

Implementors