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
    • self.run r = self r
    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.instFunctor {ρ : Type u} {m : Type v → Type w} [Functor m] :
        Equations
        • Lake.EquipT.instFunctor = { map := fun {α β : Type v} => Lake.EquipT.map, mapConst := fun {α β : Type v} => 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.instPure {ρ : Type u} {m : Type v → Type w} [Pure m] :
          Equations
          • Lake.EquipT.instPure = { pure := fun {α : Type v} => 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.instSeq {ρ : Type u} {m : Type v → Type w} [Seq m] :
              Equations
              • Lake.EquipT.instSeq = { seq := fun {α β : Type v} => Lake.EquipT.seq }
              instance Lake.EquipT.instApplicative {ρ : Type u} {m : Type v → Type w} [Applicative m] :
              Equations
              • Lake.EquipT.instApplicative = 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
              • self.bind f fetch = do let aself fetch f a fetch
              Instances For
                instance Lake.EquipT.instBind {ρ : Type u} {m : Type v → Type w} [Bind m] :
                Equations
                • Lake.EquipT.instBind = { bind := fun {α β : Type v} => Lake.EquipT.bind }
                instance Lake.EquipT.instMonad {ρ : Type u} {m : Type v → Type w} [Monad m] :
                Equations
                • Lake.EquipT.instMonad = 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.instMonadLift {ρ : Type u} {m : Type v → Type w} :
                  Equations
                  • Lake.EquipT.instMonadLift = { monadLift := fun {α : Type v} => Lake.EquipT.lift }
                  instance Lake.EquipT.instMonadFunctor {ρ : Type u} {m : Type v → Type w} :
                  Equations
                  • Lake.EquipT.instMonadFunctor = { monadMap := fun {α : Type v} (f : {β : Type v} → m βm β) (x : Lake.EquipT ρ m α) (ctx : ρ) => f (x ctx) }
                  @[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
                      instance Lake.EquipT.instAlternative {ρ : Type u} {m : Type v → Type w} [Alternative m] :
                      Equations
                      • Lake.EquipT.instAlternative = Alternative.mk (fun {α : Type v} => Lake.EquipT.failure) fun {α : Type v} => 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
                        • self.tryCatch c f = tryCatchThe ε (self f) fun (e : ε) => c e f
                        Instances For
                          instance Lake.EquipT.instMonadExceptOf {ρ : Type u} {m : Type v → Type w} (ε : Type v) [MonadExceptOf ε m] :
                          Equations
                          @[always_inline]
                          Equations
                          • One or more equations did not get rendered due to their size.