Function extern_spec_T_Option__ref_T_cloned 

pub fn extern_spec_T_Option__ref_T_cloned<T>(self_: Option<&T>) -> Option<T>
where
    T: Clone,

extern spec for Option<&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),
    _ => false
}