ULiftT.{v, u}
shrinks a monad on Type max u v
to a monad on Type u
.
Equations
- Std.Iterators.ULiftT n α = n (ULift α)
Instances For
instance
Std.Iterators.instLawfulMonadULiftT
{n : Type (max u v) → Type v'}
[Monad n]
[LawfulMonad n]
:
LawfulMonad (ULiftT n)
@[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 β) β)
:
Transforms a step of the base iterator into a step of the uLift
iterator.
Equations
- Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.Iterators.IterStep.yield it' out) = Std.Iterators.IterStep.yield { internalState := { inner := it' } } { down := out }
- Std.Iterators.Types.ULiftIterator.Monadic.modifyStep (Std.Iterators.IterStep.skip it') = Std.Iterators.IterStep.skip { internalState := { inner := it' } }
- Std.Iterators.Types.ULiftIterator.Monadic.modifyStep Std.Iterators.IterStep.done = Std.Iterators.IterStep.done
Instances For
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.
def
Std.Iterators.Types.ULiftIterator.instFinitenessRelation
{α : 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]
:
FinitenessRelation (ULiftIterator α m n β lift) n
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Std.Iterators.Types.ULiftIterator.instProductivenessRelation
{α : 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]
:
ProductivenessRelation (ULiftIterator α m n β lift) n
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Std.Iterators.Types.ULiftIterator.instIteratorLoopPartial
{α : Type u}
{m : Type u → Type u'}
{n : Type (max u v) → Type v'}
{β : Type u}
{lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ}
{o : Type (max u v) → Type u_1}
[Monad n]
[Monad o]
[Iterator α m β]
:
IteratorLoopPartial (ULiftIterator α m n β lift) n o
instance
Std.Iterators.Types.ULiftIterator.instIteratorCollect
{α : Type u}
{m : Type u → Type u'}
{n : Type (max u v) → Type v'}
{β : Type u}
{lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ}
{o : Type (max u v) → Type u_1}
[Monad n]
[Monad o]
[Iterator α m β]
:
IteratorCollect (ULiftIterator α m n β lift) n o
instance
Std.Iterators.Types.ULiftIterator.instIteratorCollectPartial
{α : Type u}
{m : Type u → Type u'}
{n : Type (max u v) → Type v'}
{β : Type u}
{lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ}
{o : Type (max u v) → Type u_1}
[Monad n]
[Monad o]
[Iterator α m β]
:
IteratorCollectPartial (ULiftIterator α m n β lift) n o
instance
Std.Iterators.Types.ULiftIterator.instIteratorSize
{α : Type u}
{m : Type u → Type u'}
{n : Type (max u v) → Type v'}
{β : Type u}
{lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ}
[Monad n]
[Iterator α m β]
[IteratorSize α m]
[Finite (ULiftIterator α m n β lift) n]
:
IteratorSize (ULiftIterator α m n β lift) n
instance
Std.Iterators.Types.ULiftIterator.instIteratorSizePartial
{α : Type u}
{m : Type u → Type u'}
{n : Type (max u v) → Type v'}
{β : Type u}
{lift : ⦃γ : Type u⦄ → m γ → ULiftT n γ}
[Monad n]
[Iterator α m β]
[IteratorSize α m]
:
IteratorSizePartial (ULiftIterator α m n β lift) n
@[inline]
def
Std.Iterators.IterM.uLift
{α : Type u}
{m : Type u → Type u'}
{β : Type u}
(it : IterM m β)
(n : Type (max u v) → Type v')
[lift : MonadLiftT m (ULiftT n)]
:
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 finiteProductive
: only if the original iterator is productive