Function vstd::array::array_index_get

source · 
pub exec fn array_index_get<T, const N: usize>(ar: &[T; N], i: usize) -> out : &T
Expand description
requires
0 <= i < N,
ensures
*out == ar@.index(i as int),