A wrapper around an iterator that provides partial consumers. See IterM.allowNontermination
.
- it : IterM m β
Instances For
@[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.