This module provides the iterator combinator IterM.take.

@[unbox]

structure Std.Iterators.Take (α : Type w) (m : Type w → Type w') (β : Type w) : Type w

The internal state of the IterM.take iterator combinator.

• remaining : Nat

  Internal implementation detail of the iterator library

• inner : IterM m β

  Internal implementation detail of the iterator library

@[inline]

def Std.Iterators.IterM.take {α : Type w} {m : Type w → Type w'} {β : Type w} (n : Nat) (it : IterM m β) : IterM m β

Given an iterator it and a natural number n, it.take n is an iterator that outputs up to the first n of it's values in order and then terminates.

Marble diagram:

it          ---a----b---c--d-e--⊥
it.take 3   ---a----b---c⊥

it          ---a--⊥
it.take 3   ---a--⊥

Termination properties:

• Finite instance: only if it is productive
• Productive instance: only if it is productive

Performance:

This combinator incurs an additional O(1) cost with each output of it.

Equations

• Std.Iterators.IterM.take n it = Std.Iterators.toIterM { remaining := n, inner := it } m β

theorem Std.Iterators.IterM.take.surjective {α : Type w} {m : Type w → Type w'} {β : Type w} (it : IterM m β) : ∃ (it₀ : IterM m β), ∃ (k : Nat), it = take k it₀

inductive Std.Iterators.Take.PlausibleStep {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] (it : IterM m β) (step : IterStep (IterM m β) β) : Prop

• yield {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} {out : β} {k : Nat} : it.internalState.inner.IsPlausibleStep (IterStep.yield it' out) → it.internalState.remaining = k + 1 → PlausibleStep it (IterStep.yield (IterM.take k it') out)
• skip {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} {it' : IterM m β} {k : Nat} : it.internalState.inner.IsPlausibleStep (IterStep.skip it') → it.internalState.remaining = k + 1 → PlausibleStep it (IterStep.skip (IterM.take (k + 1) it'))
• done {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} : it.internalState.inner.IsPlausibleStep IterStep.done → PlausibleStep it IterStep.done
• depleted {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] {it : IterM m β} : it.internalState.remaining = 0 → PlausibleStep it IterStep.done

@[inline]

instance Std.Iterators.Take.instIterator {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] : Iterator (Take α m β) m β

Equations

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

def Std.Iterators.Take.Rel {α β : Type w} (m : Type w → Type w') [Monad m] [Iterator α m β] [Productive α m] : IterM m β → IterM m β → Prop

Equations

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

theorem Std.Iterators.Take.rel_of_remaining {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] {it it' : IterM m β} (h : it'.internalState.remaining < it.internalState.remaining) : Rel m it' it

theorem Std.Iterators.Take.rel_of_inner {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] {remaining : Nat} {it it' : IterM m β} (h : it'.finitelyManySkips.Rel it.finitelyManySkips) : Rel m (IterM.take remaining it') (IterM.take remaining it)

instance Std.Iterators.Take.instFinite {α : Type w} {m : Type w → Type w'} {β : Type w} [Monad m] [Iterator α m β] [Productive α m] : Finite (Take α m β) m

instance Std.Iterators.Take.instIteratorCollect {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w} [Monad m] [Monad n] [Iterator α m β] [Productive α m] : IteratorCollect (Take α m β) m n

Equations

• Std.Iterators.Take.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

instance Std.Iterators.Take.instIteratorCollectPartial {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w} [Monad m] [Monad n] [Iterator α m β] : IteratorCollectPartial (Take α m β) m n

Equations

• Std.Iterators.Take.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

instance Std.Iterators.Take.instIteratorFor {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w} [Monad m] [Monad n] [Iterator α m β] [IteratorLoop α m n] [MonadLiftT m n] : IteratorLoop (Take α m β) m n

Equations

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

instance Std.Iterators.Take.instIteratorForPartial {α : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {β : Type w} [Monad m] [Monad n] [Iterator α m β] [IteratorLoopPartial α m n] [MonadLiftT m n] : IteratorLoopPartial (Take α m β) m n

Equations

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