vstd::slice

Function slice_index_get

Source 
pub exec fn slice_index_get<T>(slice: &[T], i: usize) -> out : &T
Expand description
requires
0 <= i < slice.view().len(),
ensures
*out == slice@.index(i as int),