Skip to main content

extern_spec_T_Option__refmut_T_cloned

Function extern_spec_T_Option__refmut_T_cloned 

Source
pub fn extern_spec_T_Option__refmut_T_cloned<T>(
    self_: Option<&mut T>,
) -> Option<T>
where T: Clone,
Expand description

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

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

ensures

match (self, result) {
    (None, None) => true,
    (Some(s), Some(r)) => T::clone.postcondition((s,), r) && ^s == *s,
    _ => false
}