Function extern_spec_T_Option_T_unwrap_or_default 

pub fn extern_spec_T_Option_T_unwrap_or_default<T>(self_: Option<T>) -> T
where
    T: Default,

extern spec for Option<T>::unwrap_or_default

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

ensures

self == None ==> T::default.postcondition((), result)

ensures

self == None || self == Some(result)