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 }