Trait IndexSpecImpl 

pub trait IndexSpecImpl<Idx>: Index<Idx>
where
    Idx: ?Sized,
{
    // Required method
    exec fn index_req(&self, index: &Idx) -> bool;
}

Required Methods

exec fn index_req(&self, index: &Idx) -> bool

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl<I: SliceIndexSpec<str>> IndexSpecImpl<I> for str

Available on verus_keep_ghost and non-verus_verify_core only.

open spec fn index_req(&self, index: &I) -> bool

{ index.in_bounds(self) }

impl<T, A: Allocator> IndexSpecImpl<usize> for VecDeque<T, A>

open spec fn index_req(&self, index: &usize) -> bool

{ *index < self.len() }

impl<T, I, const N: usize> IndexSpecImpl<I> for [T; N]

where [T]: Index<I>,

open spec fn index_req(&self, index: &I) -> bool

{ <[T] as IndexSpec<I>>::index_req(self, index) }

impl<T, I: SliceIndex<[T]>> IndexSpecImpl<I> for [T]

open spec fn index_req(&self, index: &I) -> bool

{ index.in_bounds(self) }

impl<T: Sized, I: SliceIndex<[T]>, A: Allocator> IndexSpecImpl<I> for Vec<T, A>

open spec fn index_req(&self, index: &I) -> bool

{ forall |s: &[T]| #[trigger] s@ == self@ ==> index.in_bounds(s) }

Implementors