pub fn extern_spec_T_Option__ref_T_copied<T>(self_: Option<&T>) -> Option<T>where T: Copy,
extern spec for Option<&T>::copied
Option<&T>::copied
This is not a real function: its only use is for documentation.
ghost
ensures
self