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
    @[inline]
    def Lake.EquipT.mk {ρ : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} (x : ρm α) :
    EquipT ρ m α
    Equations
    Instances For
      instance Lake.EquipT.instInhabited {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Inhabited (m α)] :
      Inhabited (EquipT ρ m α)
      Equations
      @[inline]
      def Lake.EquipT.run {ρ : Type u_1} {m : Type u_2 → Type u_3} {α : Type u_2} (self : EquipT ρ m α) (r : ρ) :
      m α
      Equations
      Instances For
        @[inline]
        def Lake.EquipT.map {m : Type u_1 → Type u_2} {α β : Type u_1} {ρ : Type u_3} [Functor m] (f : αβ) (self : EquipT ρ m α) :
        EquipT ρ m β
        Equations
        Instances For
          instance Lake.EquipT.instFunctor {m : Type u_1 → Type u_2} {ρ : Type u_3} [Functor m] :
          Equations
          @[inline]
          def Lake.EquipT.pure {m : Type u_1 → Type u_2} {α : Type u_1} {ρ : Type u_3} [Pure m] (a : α) :
          EquipT ρ m α
          Equations
          Instances For
            instance Lake.EquipT.instPure {m : Type u_1 → Type u_2} {ρ : Type u_3} [Pure m] :
            Pure (EquipT ρ m)
            Equations
            @[inline]
            def Lake.EquipT.compose {m : Type u_1 → Type u_2} {ρ : Type u_3} {α₁ α₂ β : Type u_1} (f : m α₁(Unitm α₂)m β) (x₁ : EquipT ρ m α₁) (x₂ : UnitEquipT ρ m α₂) :
            EquipT ρ m β
            Equations
            Instances For
              @[inline]
              def Lake.EquipT.seq {m : Type u_1 → Type u_2} {ρ : Type u_3} {α β : Type u_1} [Seq m] :
              EquipT ρ m (αβ)(UnitEquipT ρ m α)EquipT ρ m β
              Equations
              Instances For
                instance Lake.EquipT.instSeq {m : Type u_1 → Type u_2} {ρ : Type u_3} [Seq m] :
                Seq (EquipT ρ m)
                Equations
                instance Lake.EquipT.instApplicative {m : Type u_1 → Type u_2} {ρ : Type u_3} [Applicative m] :
                Equations
                • One or more equations did not get rendered due to their size.
                @[inline]
                def Lake.EquipT.bind {m : Type u_1 → Type u_2} {ρ : Type u_3} {α β : Type u_1} [Bind m] (self : EquipT ρ m α) (f : αEquipT ρ m β) :
                EquipT ρ m β
                Equations
                • self.bind f r = do let aself r f a r
                Instances For
                  instance Lake.EquipT.instBind {m : Type u_1 → Type u_2} {ρ : Type u_3} [Bind m] :
                  Bind (EquipT ρ m)
                  Equations
                  instance Lake.EquipT.instMonad {m : Type u_1 → Type u_2} {ρ : Type u_3} [Monad m] :
                  Monad (EquipT ρ m)
                  Equations
                  @[inline]
                  def Lake.EquipT.lift {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} (t : m α) :
                  EquipT ρ m α
                  Equations
                  Instances For
                    instance Lake.EquipT.instMonadLift {m : Type u_1 → Type u_2} {ρ : Type u_3} :
                    MonadLift m (EquipT ρ m)
                    Equations
                    instance Lake.EquipT.instMonadFunctor {m : Type u_1 → Type u_2} {ρ : Type u_3} :
                    Equations
                    @[inline]
                    def Lake.EquipT.failure {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Alternative m] :
                    EquipT ρ m α
                    Equations
                    Instances For
                      @[inline]
                      def Lake.EquipT.orElse {m : Type u_1 → Type u_2} {ρ : Type u_3} {α : Type u_1} [Alternative m] :
                      EquipT ρ m α(UnitEquipT ρ m α)EquipT ρ m α
                      Equations
                      Instances For
                        instance Lake.EquipT.instAlternative {m : Type u_1 → Type u_2} {ρ : Type u_3} [Alternative m] :
                        Equations
                        @[inline]
                        def Lake.EquipT.throw {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ : Type u_4} {α : Type u_2} [MonadExceptOf ε m] (e : ε) :
                        EquipT ρ m α
                        Equations
                        Instances For
                          @[inline]
                          def Lake.EquipT.tryCatch {ε : Type u_1} {m : Type u_2 → Type u_3} {ρ : Type u_4} {α : Type u_2} [MonadExceptOf ε m] (self : EquipT ρ m α) (c : εEquipT ρ m α) :
                          EquipT ρ m α
                          Equations
                          Instances For
                            instance Lake.EquipT.instMonadExceptOf {m : Type u_1 → Type u_2} {ρ : Type u_3} (ε : Type u_4) [MonadExceptOf ε m] :
                            Equations
                            @[inline]
                            def Lake.EquipT.tryFinally' {m : Type (max u_1 u_2) → Type u_3} {ρ : Type u_4} {α β : Type (max u_1 u_2)} [MonadFinally m] [Monad m] (x : EquipT ρ m α) (f : Option αEquipT ρ m β) :
                            EquipT ρ m (α × β)
                            Equations
                            Instances For
                              instance Lake.EquipT.instMonadFinallyOfMonad {m : Type (max u_1 u_2) → Type u_3} {ρ : Type u_4} [MonadFinally m] [Monad m] :
                              Equations