Documentation

Lake.Util.EquipT

def Lake.EquipT (ρ : Type u) (m : Type v → Type w) (α : Type v) :
Type (max u w)

A monad transformer that equips a monad with a value. This is a generalization of ReaderT where the value is not necessarily directly readable through the monad.

Equations
Instances For
    instance Lake.instInhabitedEquipT {ρ : Type u} {m : Type v → Type w} {α : Type v} [Inhabited (m α)] :
    Equations
    • Lake.instInhabitedEquipT = { default := fun x => default }
    @[inline]
    def Lake.EquipT.run {ρ : Type u} {m : Type v → Type w} {α : Type v} (self : Lake.EquipT ρ m α) (r : ρ) :
    m α
    Equations
    Instances For
      @[inline]
      def Lake.EquipT.map {ρ : Type u} {m : Type v → Type w} [Functor m] {α : Type v} {β : Type v} (f : αβ) (self : Lake.EquipT ρ m α) :
      Lake.EquipT ρ m β
      Equations
      Instances For
        instance Lake.EquipT.instFunctorEquipT {ρ : Type u} {m : Type v → Type w} [Functor m] :
        Equations
        • Lake.EquipT.instFunctorEquipT = { map := fun {α β} => Lake.EquipT.map, mapConst := fun {α β} => Lake.EquipT.map Function.const β }
        @[inline]
        def Lake.EquipT.pure {ρ : Type u} {m : Type v → Type w} [Pure m] {α : Type v} (a : α) :
        Lake.EquipT ρ m α
        Equations
        Instances For
          instance Lake.EquipT.instPureEquipT {ρ : Type u} {m : Type v → Type w} [Pure m] :
          Equations
          • Lake.EquipT.instPureEquipT = { pure := fun {α} => Lake.EquipT.pure }
          @[inline]
          def Lake.EquipT.compose {ρ : Type u} {m : Type v → Type w} {α₁ : Type v} {α₂ : Type v} {β : Type v} (f : m α₁(Unitm α₂) → m β) (x₁ : Lake.EquipT ρ m α₁) (x₂ : UnitLake.EquipT ρ m α₂) :
          Lake.EquipT ρ m β
          Equations
          Instances For
            @[inline]
            def Lake.EquipT.seq {ρ : Type u} {m : Type v → Type w} [Seq m] {α : Type v} {β : Type v} :
            Lake.EquipT ρ m (αβ)(UnitLake.EquipT ρ m α) → Lake.EquipT ρ m β
            Equations
            Instances For
              instance Lake.EquipT.instSeqEquipT {ρ : Type u} {m : Type v → Type w} [Seq m] :
              Equations
              • Lake.EquipT.instSeqEquipT = { seq := fun {α β} => Lake.EquipT.seq }
              Equations
              • Lake.EquipT.instApplicativeEquipT = Applicative.mk
              @[inline]
              def Lake.EquipT.bind {ρ : Type u} {m : Type v → Type w} [Bind m] {α : Type v} {β : Type v} (self : Lake.EquipT ρ m α) (f : αLake.EquipT ρ m β) :
              Lake.EquipT ρ m β
              Equations
              Instances For
                instance Lake.EquipT.instBindEquipT {ρ : Type u} {m : Type v → Type w} [Bind m] :
                Equations
                • Lake.EquipT.instBindEquipT = { bind := fun {α β} => Lake.EquipT.bind }
                instance Lake.EquipT.instMonadEquipT {ρ : Type u} {m : Type v → Type w} [Monad m] :
                Equations
                • Lake.EquipT.instMonadEquipT = Monad.mk
                @[inline]
                def Lake.EquipT.lift {ρ : Type u} {m : Type v → Type w} {α : Type v} (t : m α) :
                Lake.EquipT ρ m α
                Equations
                Instances For
                  instance Lake.EquipT.instMonadLiftEquipT {ρ : Type u} {m : Type v → Type w} :
                  Equations
                  • Lake.EquipT.instMonadLiftEquipT = { monadLift := fun {α} => Lake.EquipT.lift }
                  @[inline]
                  def Lake.EquipT.failure {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} :
                  Lake.EquipT ρ m α
                  Equations
                  Instances For
                    @[inline]
                    def Lake.EquipT.orElse {ρ : Type u} {m : Type v → Type w} [Alternative m] {α : Type v} :
                    Lake.EquipT ρ m α(UnitLake.EquipT ρ m α) → Lake.EquipT ρ m α
                    Equations
                    Instances For
                      Equations
                      • Lake.EquipT.instAlternativeEquipT = Alternative.mk (fun {α} => Lake.EquipT.failure) fun {α} => Lake.EquipT.orElse
                      @[inline]
                      def Lake.EquipT.throw {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (e : ε) :
                      Lake.EquipT ρ m α
                      Equations
                      Instances For
                        @[inline]
                        def Lake.EquipT.tryCatch {ρ : Type u} {m : Type v → Type w} {ε : Type v} [MonadExceptOf ε m] {α : Type v} (self : Lake.EquipT ρ m α) (c : εLake.EquipT ρ m α) :
                        Lake.EquipT ρ m α
                        Equations
                        Instances For
                          instance Lake.EquipT.instMonadExceptOfEquipT {ρ : Type u} {m : Type v → Type w} (ε : Type v) [MonadExceptOf ε m] :
                          Equations