Function vstd::array::array_len_matches_n

source · 
pub broadcast proof fn array_len_matches_n<T, const N: usize>(ar: &[T; N])
Expand description
ensures
(#[trigger] ar@.len()) == N,