Documentation

Lake.Util.Log

inductive Lake.LogLevel :
Instances For
    inductive Lake.Verbosity :
    Instances For

      Class #

      class Lake.MonadLog (m : Type u → Type v) :
      Instances
        @[inline]
        def Lake.getIsVerbose {m : TypeType u_1} [Functor m] [Lake.MonadLog m] :
        Equations
        Instances For
          @[inline]
          def Lake.getIsQuiet {m : TypeType u_1} [Functor m] [Lake.MonadLog m] :
          Equations
          Instances For
            @[inline]
            def Lake.logVerbose {m : TypeType u_1} [Monad m] [Lake.MonadLog m] (message : String) :
            Equations
            Instances For
              @[inline]
              def Lake.logInfo {m : TypeType u_1} [Monad m] [Lake.MonadLog m] (message : String) :
              Equations
              Instances For
                @[inline]
                def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                Equations
                Instances For
                  @[inline]
                  def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                  Equations
                  Instances For
                    @[specialize #[]]
                    def Lake.MonadLog.nop {m : TypeType u_1} [Pure m] :
                    Equations
                    Instances For
                      Equations
                      • Lake.MonadLog.instInhabitedMonadLog = { default := Lake.MonadLog.nop }
                      @[specialize #[]]
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[specialize #[]]
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[specialize #[]]
                          def Lake.MonadLog.lift {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLiftT m n] (self : Lake.MonadLog m) :
                          Equations
                          Instances For
                            instance Lake.MonadLog.instMonadLog {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [MonadLift m n] [methods : Lake.MonadLog m] :
                            Equations
                            @[inline]
                            def Lake.MonadLog.error {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] [Lake.MonadLog m] (msg : String) :
                            m α

                            Log the given error message and then fail.

                            Equations
                            Instances For

                              Transformers #

                              @[inline, reducible]
                              abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) :
                              Type (max v w)
                              Equations
                              Instances For
                                instance Lake.instInhabitedMonadLogT {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] :
                                Equations
                                • Lake.instInhabitedMonadLogT = { default := fun x => pure default }
                                instance Lake.instMonadLogMonadLogT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[inline]
                                def Lake.MonadLogT.adaptMethods {n : Type u_1 → Type u_2} {m : Type u_3 → Type u_1} {m' : Type u_4 → Type u_1} {α : Type u_1} [Monad n] (f : Lake.MonadLog mLake.MonadLog m') (self : Lake.MonadLogT m' n α) :
                                Equations
                                Instances For
                                  @[inline]
                                  def Lake.MonadLogT.ignoreLog {m : TypeType u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : Lake.MonadLogT m n α) :
                                  n α
                                  Equations
                                  Instances For
                                    @[inline, reducible]
                                    abbrev Lake.LogIO (α : Type) :
                                    Equations
                                    Instances For
                                      Equations
                                      Equations
                                      @[inline, reducible]
                                      abbrev Lake.LogT (m : TypeType) (α : Type) :
                                      Equations
                                      Instances For