Skip to main content

extern_spec_T_E_Result__ref_T_E_copied

creusot_std::std::result

Function extern_spec_T_E_Result__ref_T_E_copied 

Source 
pub fn extern_spec_T_E_Result__ref_T_E_copied<T, E>(
    self_: Result<&T, E>,
) -> Result<T, E>
where
    T: Copy,
Expand description

extern spec for Result<&T, E>::copied

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

ghost

ensures 

self

ensures 

self