@[inline]
def
Std.Iterators.Iter.attachWith
{α β : Type w}
[Iterator α Id β]
(it : Iter β)
(P : β → Prop)
(h : ∀ (out : β), it.IsPlausibleIndirectOutput 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 finiteProductive
instance: only if the base iterator is productive
Equations
- it.attachWith P h = (it.toIterM.attachWith P ⋯).toIter