Skip to main content

_verus_external_fn_specification_0__60__32__38__32__39_a_32__91_T_59__32_N_93__32_as_32_core_32__58__58__32_iter_32__58__58__32_IntoIterator_32__62__32__58__58__32_into__iter

vstd::array

Function _verus_external_fn_specification_0__60__32__38__32__39_a_32__91_T_59__32_N_93__32_as_32_core_32__58__58__32_iter_32__58__58__32_IntoIterator_32__62__32__58__58__32_into__iter 

Source 
pub unsafe exec fn _verus_external_fn_specification_0__60__32__38__32__39_a_32__91_T_59__32_N_93__32_as_32_core_32__58__58__32_iter_32__58__58__32_IntoIterator_32__62__32__58__58__32_into__iter<'a, T, const N: usize>(
    s: &'a [T; N],
) -> iter : Iter<'a, T>
Expand description
ensures
IteratorSpec::remaining(&iter) == s@.as_ref(),
IteratorSpec::decrease(&iter) is Some,

Specification for <&'a [T; N] as core::iter::IntoIterator>::into_iter