Documentation

Std.Data.Iterators.Combinators.Take

@[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.

Equations
Instances For