Documentation

Init.Data.Iterators.Combinators.Attach

@[inline]
def Std.Iterators.Iter.attachWith {α β : Type w} [Iterator α Id β] (it : Iter β) (P : βProp) (h : ∀ (out : β), it.IsPlausibleIndirectOutput outP out) :
Iter { out : β // P out }

“Attaches” individual proofs to an iterator of values that satisfy a predicate P, returning an iterator with values in the corresponding subtype { x // P x }.

Termination properties:

  • Finite instance: only if the base iterator is finite
  • Productive instance: only if the base iterator is productive
Equations
Instances For