@[implicit_reducible]

def Std.Iterators.ULiftT (n : Type (max u v) → Type v') (α : Type u) : Type v'

ULiftT.{v, u} shrinks a monad on Type max u v to a monad on Type u.

Equations

• Std.Iterators.ULiftT n α = n (ULift α)

@[inline]

def Std.Iterators.ULiftT.run {n : Type (max u v) → Type v'} {α : Type u} (x : ULiftT n α) : n (ULift α)

Returns the underlying n-monadic representation of a ULiftT n α value.

Equations

• x.run = x

@[instance_reducible]

instance Std.Iterators.instMonadULiftT {n : Type (max u v) → Type v'} [Monad n] : Monad (ULiftT n)

Equations

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

instance Std.Iterators.instLawfulMonadULiftT {n : Type (max u v) → Type v'} [Monad n] [LawfulMonad n] : LawfulMonad (ULiftT n)

@[simp]

theorem Std.Iterators.ULiftT.run_pure {n : Type (max u v) → Type v'} [Monad n] {α : Type u} {a : α} : (pure a).run = pure { down := a }

@[simp]

theorem Std.Iterators.ULiftT.run_bind {n : Type (max u v) → Type v'} [Monad n] {α β : Type u} {x : ULiftT n α} {f : α → ULiftT n β} : (x >>= f).run = do let a ← x.run (f a.down).run

@[simp]

theorem Std.Iterators.ULiftT.run_map {n : Type (max u v) → Type v'} [Monad n] {α β : Type u} {x : ULiftT n α} {f : α → β} : (f <$> x).run = do let a ← x.run pure { down := f a.down }

@[unbox]

structure Std.Iterators.Types.ULiftIterator (α : Type u) (m : Type u → Type u') (n : Type (max u v) → Type v') (β : Type u) (lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ) : Type (max u v)

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

• inner : IterM m β

@[inline]

def Std.Iterators.Types.ULiftIterator.Monadic.modifyStep {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ} (step : IterStep (IterM m β) β) : IterStep (IterM n (ULift β)) (ULift β)

Transforms a step of the base iterator into a step of the uLift iterator.

Equations

• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.IterStep.yield it' out) = Std.IterStep.yield { internalState := { inner := it' } } { down := out }
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.IterStep.skip it') = Std.IterStep.skip { internalState := { inner := it' } }
• Std.Iterators.Types.ULiftIterator.Monadic.modifyStep Std.IterStep.done = Std.IterStep.done

@[instance_reducible]

instance Std.Iterators.Types.ULiftIterator.instIterator {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ} [Iterator α m β] [Monad n] : Iterator (ULiftIterator α m n β lift) n (ULift β)

Equations

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

instance Std.Iterators.Types.ULiftIterator.instFinite {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ} [Iterator α m β] [Finite α m] [Monad n] : Finite (ULiftIterator α m n β lift) n

instance Std.Iterators.Types.ULiftIterator.instProductive {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ} [Iterator α m β] [Productive α m] [Monad n] : Productive (ULiftIterator α m n β lift) n

@[instance_reducible]

instance Std.Iterators.Types.ULiftIterator.instIteratorLoop {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} {lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ} {o : Type x → Type x'} [Monad n] [Monad o] [Iterator α m β] : IteratorLoop (ULiftIterator α m n β lift) n o

Equations

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

@[inline]

def Std.IterM.uLift {α β : Type u} {m : Type u → Type u'} (it : IterM m β) (n : Type (max u v) → Type v') [lift : MonadLiftT m (Iterators.ULiftT n)] : IterM n (ULift β)

Transforms an m-monadic iterator with values in β into an n-monadic iterator with values in ULift β. Requires a MonadLift m (ULiftT n) instance.

Marble diagram:

it            ---a    ----b    ---c    --d    ---⊥
it.uLift n    ---.up a----.up b---.up c--.up d---⊥

Termination properties:

• Finite: only if the original iterator is finite
• Productive: only if the original iterator is productive

Equations

• it.uLift n = { internalState := { inner := it } }