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

A wrapper around an iterator that provides partial consumers. See IterM.allowNontermination.

• it : IterM m β

@[inline]

def Std.Iterators.IterM.allowNontermination {α : Type w} {m : Type w → Type w'} {β : Type w} (it : IterM m β) : Partial m β

For an iterator it, it.allowNontermination provides potentially nonterminating variants of consumers such as toList. They can be used without any proof of termination such as Finite or Productive, but as they are implemented with the partial declaration modifier, they are opaque for the kernel and it is impossible to prove anything about them.

Equations

• it.allowNontermination = { it := it }