This file provides an empty iterator.

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

The internal state of the IterM.empty iterator.

@[inline]

def Std.Iterators.IterM.empty (m : Type w → Type w') (β : Type w) : IterM m β

Returns an iterator that terminates immediately.

Termination properties:

• Finite instance: always
• Productive instance: always

Equations

• Std.Iterators.IterM.empty m β = Std.Iterators.toIterM { } m β

def Std.Iterators.Empty.PlausibleStep {m : Type w → Type w'} {β : Type w} : IterM m β → (step : IterStep (IterM m β) β) → Prop

Equations

• Std.Iterators.Empty.PlausibleStep x✝ step = (step = Std.Iterators.IterStep.done)

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

Equations

• Std.Iterators.Empty.instIterator = { IsPlausibleStep := Std.Iterators.Empty.PlausibleStep, step := fun (x : Std.IterM m β) => pure (Std.Iterators.PlausibleIterStep.done ⋯) }

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

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

Equations

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

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

Equations

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

instance Std.Iterators.Empty.instIteratorLoop {m : Type w → Type w'} {β : Type w} {n : Type w → Type w''} [Monad m] [Monad n] : IteratorLoop (Empty m β) m n

Equations

• Std.Iterators.Empty.instIteratorLoop = Std.Iterators.IteratorLoop.defaultImplementation

instance Std.Iterators.Empty.instIteratorLoopPartial {m : Type w → Type w'} {β : Type w} {n : Type w → Type w''} [Monad m] [Monad n] : IteratorLoopPartial (Empty m β) m n

Equations

• Std.Iterators.Empty.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation