Function extern_spec_T_Option_T_zip 

pub fn extern_spec_T_Option_T_zip<T, U>(
    self_: Option<T>,
    other: Option<U>,
) -> Option<(T, U)>

extern spec for Option<T>::zip

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

terminates

ghost

ensures

match (self, other) {
    (None, _)          => result == None && resolve(other),
    (_, None)          => result == None && resolve(self),
    (Some(t), Some(u)) => result == Some((t, u)),
}