Function extern_spec_I_IntoIterator_I_into_iter 

pub fn extern_spec_I_IntoIterator_I_into_iter<I: Iterator>(self_: I) -> I

extern spec for [I::into_iter]

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

terminates

ghost

ensures

result == self