Skip to main content

extern_spec_T_E_Result_T_E_expect

creusot_std::std::result

Function extern_spec_T_E_Result_T_E_expect 

Source 
pub fn extern_spec_T_E_Result_T_E_expect<T, E>(
    self_: Result<T, E>,
    msg: &str,
) -> T
where
    E: Debug,
Expand description

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

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

terminates

ghost

requires 

exists<t: T> self == Ok(t)

ensures 

Ok(result) == self