Function vstd::std_specs::vec::vec_index

source · 
pub exec fn vec_index<T, A: Allocator>(vec: &Vec<T, A>, i: usize) -> &T
Expand description
requires
i < vec.view().len(),
ensures
*element == vec.view().index(i as int),

This is a specification for the indexing operator vec[i]