pub trait VecAdditionalSpecFns<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, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A>
impl<T, A: Allocator> VecAdditionalSpecFns<T> for Vec<T, A>
Source§open spec fn spec_index(&self, i: int) -> T
open spec fn spec_index(&self, i: int) -> T
{ self.view().index(i) }