Function extern_spec_T_E_Result_T_E_unwrap_or 

pub fn extern_spec_T_E_Result_T_E_unwrap_or<T, E>(
    self_: Result<T, E>,
    default: T,
) -> T

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

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

terminates

ghost

ensures

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

ensures

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