Documentation

Init.Data.Iterators.Combinators.Monadic.ULift

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
Instances For
    @[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
    Instances For
      instance Std.Iterators.instMonadULiftT {n : Type (max u v) → Type v'} [Monad n] :
      Equations
      • One or more equations did not get rendered due to their size.
      @[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 ax.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 ax.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.

      Instances For
        @[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
        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] :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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
            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] :
            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.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
              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
              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
              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 β] :
              Equations
              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
              @[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
              Instances For