vstd::array

Function lemma_array_index

Source
pub broadcast proof fn lemma_array_index<T, const N: usize>(a: [T; N], i: int)
Expand description
requires
0 <= i < N,
ensures
a[i] == array_view(a)[i],