Trait ExecSpecSeqIndexOfFirst 

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

    // Required method
    exec fn exec_index_of_first(self, needle: Self::Elem) -> Option<usize>;
}

Spec for executable version of Seq::index_of_first.

Required Associated Types

type Elem: DeepView

Required Methods

exec fn exec_index_of_first(self, needle: Self::Elem) -> Option<usize>

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 + PartialEq> ExecSpecSeqIndexOfFirst<'a> for &'a [T]

where &'a T: ExecSpecEq<'a, Other = &'a T>,

exec fn exec_index_of_first(self, needle: Self::Elem) -> res : Option<usize>

ensures

match res {
    Some(i) => {
        self.deep_view().index_of_first(needle.deep_view()).is_some()
            && i as int == self.deep_view().index_of_first(needle.deep_view())->0
    }
    None => self.deep_view().index_of_first(needle.deep_view()) == None::<int>,
},

type Elem = T

Implementors