Skip to main content

extern_spec_T_E_Result_T_E_ok

creusot_std::std::result

Function extern_spec_T_E_Result_T_E_ok 

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

extern spec for Result<T, E>::ok

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

ghost

ensures 

self

ensures 

(exists<e: E> self == Err(e)) ==> result == None