vstd::array

Function axiom_spec_array_as_slice

Source 
pub broadcast proof fn axiom_spec_array_as_slice<T, const N: usize>(ar: &[T; N])
Expand description
ensures
(#[trigger] spec_array_as_slice(ar))@ == ar@,