SliceIndexSpecImpl

Trait SliceIndexSpecImpl

pub trait SliceIndexSpecImpl<T>: SliceIndex<T>where
    T: ?Sized,{
    // Required method
    exec fn index_req(&self, slice: &T) -> bool;
}

Required Methods§

exec fn index_req(&self, slice: &T) -> bool

Implementations on Foreign Types§

impl<T> SliceIndexSpecImpl<[T]> for usize

open spec fn index_req(&self, slice: &[T]) -> bool

{ *self < slice@.len() }

impl<T> SliceIndexSpecImpl<[T]> for Range<usize>

open spec fn index_req(&self, slice: &[T]) -> bool

{
    &&& self.start <= self.end
    &&& self.end <= slice@.len()

}

Implementors§