Function extern_spec_T_E_Result_T_E_as_mut 

pub fn extern_spec_T_E_Result_T_E_as_mut<T, E>(
    self_: &mut Result<T, E>,
) -> Result<&mut T, &mut E>

extern spec for Result<T, E>::as_mut

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

terminates

ghost

ensures

exists<t: &mut T> *self == Ok(*t) && ^self == Ok(^t) && result == Ok(t) ||
exists<e: &mut E> *self == Err(*e) && ^self == Err(^e) && result == Err(e)