Trait vstd::slice::SliceAdditionalSpecFns
source · pub trait SliceAdditionalSpecFns<T>: View<V = Seq<T>> {
// Required method
spec fn spec_index(&self, i: int) -> T;
}
Required Methods§
sourcespec fn spec_index(&self, i: int) -> T
spec fn spec_index(&self, i: int) -> T
recommends
0 <= i < self.view().len(),
Implementations on Foreign Types§
source§impl<T> SliceAdditionalSpecFns<T> for [T]
impl<T> SliceAdditionalSpecFns<T> for [T]
source§open spec fn spec_index(&self, i: int) -> T
open spec fn spec_index(&self, i: int) -> T
{ self.view().index(i) }