Function extern_spec_T_Option_T_or

pub fn extern_spec_T_Option_T_or<T>(
    self_: Option<T>,
    optb: Option<T>,
) -> Option<T>

Expand description

extern spec for Option<T>::or

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

terminates

ghost

ensures

self == None ==> result == optb

ensures

self == None || (result == self && resolve(optb))

extern_spec_T_Option_T_or