@[inline]

def Std.Iterators.Iter.take {α β : Type w} (n : Nat) (it : Iter β) : Iter β

Given an iterator it and a natural number n, it.take n is an iterator that outputs up to the first n of it's values in order and then terminates.

Marble diagram:

it          ---a----b---c--d-e--⊥
it.take 3   ---a----b---c⊥

it          ---a--⊥
it.take 3   ---a--⊥

Termination properties:

• Finite instance: only if it is productive
• Productive instance: only if it is productive

Performance:

This combinator incurs an additional O(1) cost with each output of it.