structure Std.IterM.Total {α : Type w} (m : Type w → Type w') (β : Type w) : Type w

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

• it : IterM m β

  The wrapped iterator, which was wrapped by IterM.ensureTermination.

@[inline]

def Std.IterM.ensureTermination {α β : Type w} {m : Type w → Type w'} (it : IterM m β) : Total m β

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

Equations

• it.ensureTermination = { it := it }