@[inline]
def
Std.Iterators.Iter.zip
{α₁ β₁ α₂ β₂ : Type w}
[Iterator α₁ Id β₁]
[Iterator α₂ Id β₂]
(left : Iter β₁)
(right : 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 eitherleft
orright
is finite and the other is productiveProductive
instance: only ifleft
andright
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.