Function vstd::array::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@,