@[unbox]

structure Std.Iterators.Types.Attach (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (P : β → Prop) : Type w

Internal state of the attachWith combinator. Do not depend on its internals.

• inner : IterM m β
• invariant (out : β) : self.inner.IsPlausibleIndirectOutput out → P out

@[inline]

def Std.Iterators.Types.Attach.Monadic.modifyStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {P : β → Prop} (it : IterM m { out : β // P out }) (step : it.internalState.inner.Step) : IterStep (IterM m { out : β // P out }) { out : β // P out }

instance Std.Iterators.Types.Attach.instIterator {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] {P : β → Prop} : Iterator (Attach α m P) m { out : β // P out }

def Std.Iterators.Types.Attach.instFinitenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] {P : β → Prop} : FinitenessRelation (Attach α m P) m

instance Std.Iterators.Types.Attach.instFinite {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Finite α m] {P : β → Prop} : Finite (Attach α m P) m

def Std.Iterators.Types.Attach.instProductivenessRelation {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Productive α m] {P : β → Prop} : ProductivenessRelation (Attach α m P) m

instance Std.Iterators.Types.Attach.instProductive {α β : Type w} {m : Type w → Type w'} [Monad m] [Iterator α m β] [Productive α m] {P : β → Prop} : Productive (Attach α m P) m

instance Std.Iterators.Types.Attach.instIteratorCollect {n : Type w → Type u_1} {α β : Type w} {m : Type w → Type w'} [Monad m] [Monad n] {P : β → Prop} [Iterator α m β] : IteratorCollect (Attach α m P) m n

instance Std.Iterators.Types.Attach.instIteratorCollectPartial {n : Type w → Type u_1} {α β : Type w} {m : Type w → Type w'} [Monad m] [Monad n] {P : β → Prop} [Iterator α m β] : IteratorCollectPartial (Attach α m P) m n

instance Std.Iterators.Types.Attach.instIteratorLoop {n : Type w → Type u_1} {α β : Type w} {m : Type w → Type w'} [Monad m] [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] : IteratorLoop (Attach α m P) m n

instance Std.Iterators.Types.Attach.instIteratorLoopPartial {n : Type w → Type u_1} {α β : Type w} {m : Type w → Type w'} [Monad m] [Monad n] {P : β → Prop} [Iterator α m β] [MonadLiftT m n] : IteratorLoopPartial (Attach α m P) m n

instance Std.Iterators.Types.instIteratorSizeAttachSubtype {α β : Type w} {m : Type w → Type w'} [Monad m] {P : β → Prop} [Iterator α m β] [IteratorSize α m] : IteratorSize (Attach α m P) m

instance Std.Iterators.Types.instIteratorSizePartialAttachSubtype {α β : Type w} {m : Type w → Type w'} [Monad m] {P : β → Prop} [Iterator α m β] [IteratorSizePartial α m] : IteratorSizePartial (Attach α m P) m

@[inline]

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