Function extern_spec_T_Option_T_iter 

pub fn extern_spec_T_Option_T_iter<T>(self_: &Option<T>) -> Iter<'_, T>

extern spec for Option<T>::iter

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

ensures

match *self {
    None => exists<it: &mut Iter<'_, T>> it.completed() && *it == result,
    Some(x) => exists<s: Seq<&T>, it: &mut Iter<'_, T>> {
        it.completed() && s.len() == 1 && *s[0] == x && result.produces(s, *it)
    }
}