Function extern_spec_T_E_Result_T_E_or 

pub fn extern_spec_T_E_Result_T_E_or<T, E, F>(
    self_: Result<T, E>,
    res: Result<T, F>,
) -> Result<T, F>

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

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

terminates

ghost

ensures

forall<t: T> self == Ok(t) ==> result == Ok(t)

ensures

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