structure Std.Iterators.Iter.Total {α : Type w} (β : Type w) : Type w

A wrapper around an iterator that provides strictly terminating consumers. See Iter.ensureTermination.

• it : Iter β

@[inline]

def Std.Iterators.Iter.ensureTermination {α β : Type w} (it : Iter β) : Total β

For an iterator it, it.ensureTermination provides variants of consumers that always terminate.

Equations

• it.ensureTermination = { it := it }