Function extern_spec_T_Option_T_as_deref_mut 

pub fn extern_spec_T_Option_T_as_deref_mut<T>(
    self_: &mut Option<T>,
) -> Option<&mut <T as Deref>::Target>
where
    T: DerefMut,

extern spec for Option<T>::as_deref_mut

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

requires

match *self {
    None => true,
    Some(cur) => forall<bor: &mut T> *bor == cur ==> T::deref_mut.precondition((bor,)),
}

ensures

match (*self, ^self, result) {
    (None, None, None) => true,
    (Some(cur), Some(fin), Some(r)) => exists<bor: &mut T> *bor == cur && ^bor == fin && T::deref_mut.postcondition((bor,), r),
    _ => false,
}