@[inline]

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

Given an iterator it and a natural number n, it.drop n is an iterator that forwards all of it's output values except for the first n.

Marble diagram:

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

it          ---a--⊥
it.drop 3   ------⊥

Termination properties:

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

Performance:

Currently, this combinator incurs an additional O(1) cost with each output of it, even when the iterator does not drop any elements anymore.

Equations

• Std.Iterators.Iter.drop n it = (Std.Iterators.IterM.drop n it.toIterM).toIter