source

inductive Lake.LogLevel :

Type

Instances For

source

inductive Lake.Verbosity :

Type u

Instances For

source

instance Lake.instBEqVerbosity :

BEq Lake.Verbosity

source

instance Lake.instInhabitedVerbosity :

Inhabited Lake.Verbosity

Class #

source

class Lake.MonadLog (m : Type u → Type v) :

Type v

getVerbosity : m Lake.Verbosity
log : String → Lake.LogLevel → m PUnit

Instances

source

@[inline]

def Lake.getIsVerbose {m : Type → Type u_1} [Functor m] [Lake.MonadLog m] :

m Bool

Instances For

source

@[inline]

def Lake.getIsQuiet {m : Type → Type u_1} [Functor m] [Lake.MonadLog m] :

m Bool

Instances For

source

@[inline]

def Lake.logVerbose {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] (message : String) :

m PUnit

Instances For

source

@[inline]

def Lake.logInfo {m : Type → Type u_1} [Monad m] [Lake.MonadLog m] (message : String) :

m PUnit

Instances For

source

@[inline]

def Lake.logWarning {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :

m PUnit

Instances For

source

@[inline]

def Lake.logError {m : Type u_1 → Type u_2} [Lake.MonadLog m] (message : String) :

m PUnit

Instances For

source

@[specialize #[]]

def Lake.MonadLog.nop {m : Type → Type u_1} [Pure m] :

Lake.MonadLog m

Instances For

source

instance Lake.MonadLog.instInhabitedMonadLog {m : Type → Type u_1} [Pure m] :

Inhabited (Lake.MonadLog m)

source

@[specialize #[]]

def Lake.MonadLog.io {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Instances For

source

@[specialize #[]]

def Lake.MonadLog.eio {m : Type → Type u_1} [MonadLiftT BaseIO m] (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

Lake.MonadLog m

Instances For

source

@[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) :

Lake.MonadLog n

Instances For

source

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] :

Lake.MonadLog n

source

@[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 #

source

@[inline, reducible]

abbrev Lake.MonadLogT (m : Type u → Type v) (n : Type v → Type w) (α : Type v) :

Type (max v w)

Instances For

source

instance Lake.instInhabitedMonadLogT {n : Type u_1 → Type u_2} {α : Type u_1} {m : Type u_3 → Type u_1} [Pure n] [Inhabited α] :

Inhabited (Lake.MonadLogT m n α)

source

instance Lake.instMonadLogMonadLogT {n : Type u_1 → Type u_2} {m : Type u_1 → Type u_1} [Monad n] [MonadLiftT m n] :

Lake.MonadLog (Lake.MonadLogT m n)

source

@[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 m → Lake.MonadLog m') (self : Lake.MonadLogT m' n α) :

Lake.MonadLogT m n α

Instances For

source

@[inline]

def Lake.MonadLogT.ignoreLog {m : Type → Type u_1} {n : Type u_1 → Type u_2} {α : Type u_1} [Pure m] (self : Lake.MonadLogT m n α) :

n α

Instances For

source

@[inline, reducible]

abbrev Lake.LogIO (α : Type) :

Type

Instances For

source

instance Lake.instMonadErrorLogIO :

Lake.MonadError Lake.LogIO

source

instance Lake.instMonadLiftIOLogIO :

MonadLift IO Lake.LogIO

source

def Lake.LogIO.captureLog {α : Type} (self : Lake.LogIO α) (verbosity : optParam Lake.Verbosity Lake.Verbosity.normal) :

BaseIO (String × Option α)

Instances For

source

@[inline, reducible]

abbrev Lake.LogT (m : Type → Type) (α : Type) :

Type

Instances For