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] :
        Instances For
          @[inline]
          def Lake.getIsQuiet {m : TypeType u_1} [Functor m] [Lake.MonadLog m] :
          Instances For
            @[inline]
            def Lake.logVerbose {m : TypeType u_1} [Monad m] [Lake.MonadLog m] (message : String) :
            Instances For
              @[inline]
              def Lake.logInfo {m : TypeType u_1} [Monad m] [Lake.MonadLog m] (message : String) :
              Instances For
                @[inline]
                def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                Instances For
                  @[inline]
                  def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :
                  Instances For
                    @[specialize #[]]
                    def Lake.MonadLog.nop {m : TypeType u_1} [Pure m] :
                    Instances For
                      @[specialize #[]]
                      Instances For
                        @[specialize #[]]
                        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) :
                          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] :
                            @[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.

                            Instances For

                              Transformers #

                              @[inline, reducible]
                              abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) :
                              Type (max v w)
                              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 α] :
                                instance Lake.instMonadLogMonadLogT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] :
                                @[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 α) :
                                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 α
                                  Instances For
                                    @[inline, reducible]
                                    abbrev Lake.LogIO (α : Type) :
                                    Instances For
                                      @[inline, reducible]
                                      abbrev Lake.LogT (m : TypeType) (α : Type) :
                                      Instances For