Function extern_spec_std_iter_Iterator_zip 

pub fn extern_spec_std_iter_Iterator_zip<Self_, U: IntoIterator>(
    self_: Self_,
    other: U,
) -> Zip<Self_, U::IntoIter>
where
    Self_: Sized + IteratorSpec + ?Sized + Iterator,
    U::IntoIter: Iterator,

extern spec for ::std::iter::Iterator::zip<U>

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

terminates

ghost

requires

U::into_iter.precondition((other,))

ensures

result.itera() == self

ensures

U::into_iter.postcondition((other,), result.iterb())