Function extern_spec_T_Option_T_iter_mut 

pub fn extern_spec_T_Option_T_iter_mut<T>(
    self_: &mut Option<T>,
) -> IterMut<'_, T>

extern spec for Option<T>::iter_mut

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

ensures

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