Skip to main content

extern_spec_T_E_Result_Option_T_E_transpose

creusot_std::std::result

Function extern_spec_T_E_Result_Option_T_E_transpose 

Source 
pub fn extern_spec_T_E_Result_Option_T_E_transpose<T, E>(
    self_: Result<Option<T>, E>,
) -> Option<Result<T, E>>
Expand description

extern spec for Result<Option<T>, E>::transpose

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

ghost

ensures 

self

ensures 

self

ensures 

self