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()

}

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

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

{ self.start <= slice@.len() }

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

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

{ true }

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

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

{ slice_range_valid(self, slice@.len()) }

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

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

{ self.end <= slice@.len() }

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

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

{ self.end < slice@.len() }

Implementors