Function extern_spec_T_IntoIterator__refmut_Option_T_into_iter 

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

extern spec for <&mut Option<T> as IntoIterator>::into_iter

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

terminates

ghost

ensures

*self == match result@ { None => None, Some(r) => Some(*r) }

ensures

^self == match result@ { None => None, Some(r) => Some(^r) }