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.

ghost

ensures

self

ensures

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