Documentation

Std.Data.Iterators.Consumers.Monadic.Partial

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

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

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.

    Equations
    Instances For