Function extern_spec_T_Option_T_xor 

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

extern spec for Option<T>::xor

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

terminates

ghost

ensures

match (self, optb) {
    (None, None)         => result == None,
    (Some(t1), Some(t2)) => result == None && resolve(t1) && resolve(t2),
    (Some(t), None)      => result == Some(t),
    (None, Some(t))      => result == Some(t),
}