Function extern_spec_T_Option__refmut_T_copied 

pub fn extern_spec_T_Option__refmut_T_copied<T>(
    self_: Option<&mut T>,
) -> Option<T>
where
    T: Copy,

extern spec for Option<&mut T>::copied

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

terminates

ghost

ensures

match self {
    None => result == None,
    Some(s) => result == Some(*s) && ^s == *s
}