IndexSpecImpl

vstd::std_specs::core

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

Implementations on Foreign Types§

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.index_req(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.index_req(s) }

Implementors§