@[inline]

def Std.Iter.attachWith {α β : Type w} [Iterator α Id β] (it : Iter β) (P : β → Prop) (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P 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

• it.attachWith P h = (it.toIterM.attachWith P ⋯).toIter