Function extern_spec_T_E_Result__refmut_T_E_copied 

pub fn extern_spec_T_E_Result__refmut_T_E_copied<T, E>(
    self_: Result<&mut T, E>,
) -> Result<T, E>
where
    T: Copy,

extern spec for Result<&mut T, E>::copied

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

terminates

ghost

ensures

forall<t: &mut T> self == Ok(t) ==> result == Ok(*t) && resolve(t)

ensures

forall<e: E> self == Err(e) ==> result == Err(e)