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

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

- it : Iter β

Instances For

source
@[inline]
def Std.Iterators.Iter.allowNontermination {α β : Type w} (it : Iter β) :
Partial β

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 }

Instances For