Function extern_spec_T_Iterator_Iter_T_next 

pub fn extern_spec_T_Iterator_Iter_T_next<'a, T>(
    self_: &mut Iter<'a, T>,
) -> Option<&'a T>

extern spec for Iter<'a, T>::next

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

ghost

ensures

match result {
    None => self.completed(),
    Some(v) => (*self).produces(Seq::singleton(v), ^self)
}