@[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 }

Equations

• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.Iterators.IterStep.yield it' out, h⟩ = Std.Iterators.IterStep.yield { internalState := { inner := it', invariant := ⋯ } } ⟨out, ⋯⟩
• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.Iterators.IterStep.skip it', h⟩ = Std.Iterators.IterStep.skip { internalState := { inner := it', invariant := ⋯ } }
• Std.Iterators.Types.Attach.Monadic.modifyStep it ⟨Std.Iterators.IterStep.done, property⟩ = Std.Iterators.IterStep.done

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 }

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Std.Iterators.Types.Attach.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

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

Equations

• Std.Iterators.Types.Attach.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

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

Equations

• Std.Iterators.Types.Attach.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

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

Equations

• Std.Iterators.Types.Attach.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

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

Equations

• Std.Iterators.Types.instIteratorSizeAttachSubtype = { size := fun (it : Std.IterM m { out : β // P out }) => Std.Iterators.IteratorSize.size it.internalState.inner }

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

Equations

• Std.Iterators.Types.instIteratorSizePartialAttachSubtype = { size := fun (it : Std.IterM m { out : β // P out }) => Std.Iterators.IteratorSizePartial.size it.internalState.inner }

@[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

Equations

• it.attachWith P h = { internalState := { inner := it, invariant := h } }