Function extern_spec_T__slice_T_iter 

pub fn extern_spec_T__slice_T_iter<T>(self_: &[T]) -> Iter<'_, T>

extern spec for slice<T>::iter

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

result@ == self