@[inline]

def Std.Iterators.Iter.zip {α₁ β₁ α₂ β₂ : Type w} [Iterator α₁ Id β₁] [Iterator α₂ Id β₂] (left : Iter β₁) (right : Iter β₂) : Iter (β₁ × β₂)

Given two iterators left and right, left.zip right is an iterator that yields pairs of outputs of left and right. When one of them terminates, the zip iterator will also terminate.

Marble diagram:

left               --a        ---b        --c
right                 --x         --y        --⊥
left.zip right     -----(a, x)------(b, y)-----⊥

Termination properties:

• Finite instance: only if either left or right is finite and the other is productive
• Productive instance: only if left and right are productive

There are situations where left.zip right is finite (or productive) but none of the instances above applies. For example, if left immediately terminates but right always skips, then left.zip.right is finite even though no Finite (or even Productive) instance is available. Such instances need to be proved manually.

Performance:

This combinator incurs an additional O(1) cost with each step taken by left or right.

Right now, the compiler does not unbox the internal state, leading to worse performance than theoretically possible.