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