@[inline]

def Std.Iter.take {α β : Type w} [Iterator α Id β] (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.

@[inline]

def Std.Iter.toTake {α β : Type w} [Iterator α Id β] [Iterators.Finite α Id] (it : Iter β) : Iter β

This combinator is only useful for advanced use cases.

Given a finite iterator it, returns an iterator that behaves exactly like it but is of the same type as it.take n.

Marble diagram:

it          ---a----b---c--d-e--⊥
it.toTake   ---a----b---c--d-e--⊥

Termination properties:

• Finite instance: always
• Productive instance: always

Performance:

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