vstd::std_specs::vec

Trait VecAdditionalSpecFns

Source
pub trait VecAdditionalSpecFns<T>: View<V = Seq<T>> {
    // Required method
    spec fn spec_index(&self, i: int) -> T;
}

Required Methods§

Source

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>

Source§

open spec fn spec_index(&self, i: int) -> T

{ self.view().index(i) }

Implementors§