Function extern_spec_std_option_T_Option_T_zip 

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

extern spec for ::std::option::Option<T>::zip<U>

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)),
                }