Init.Data.Iterators.Combinators.Monadic.ULift

source

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 α)

Instances For

source

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

source

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.

source

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

LawfulMonad (ULiftT n)

source

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

source

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

source

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

source

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

Instances For

source

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

source

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.

source

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.

source

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

source

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.

source

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

source

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 (max u v) → Type u_1} [Monad n] [Monad o] [Iterator α m β] :

IteratorLoop (ULiftIterator α m n β lift) n o

Equations

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

source

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

Equations

Std.Iterators.Types.ULiftIterator.instIteratorLoopPartial = Std.Iterators.IteratorLoopPartial.defaultImplementation

source

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

Equations

Std.Iterators.Types.ULiftIterator.instIteratorCollect = Std.Iterators.IteratorCollect.defaultImplementation

source

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

Equations

Std.Iterators.Types.ULiftIterator.instIteratorCollectPartial = Std.Iterators.IteratorCollectPartial.defaultImplementation

source

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

Equations

Std.Iterators.Types.ULiftIterator.instIteratorSize = Std.Iterators.IteratorSize.defaultImplementation

source

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

Equations

Std.Iterators.Types.ULiftIterator.instIteratorSizePartial = Std.Iterators.IteratorSizePartial.defaultImplementation

source

@[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)] :

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