IdrisDoc: Effect.Logging.Default

Effect.Logging.Default

The default logging effect that allows messages to be logged at
different numerical levels. The higher the number the greater in
verbosity the logging.

In this effect the resource we are computing over is the logging
level itself.

warn : String -> Eff () [LOG]
trace : String -> Eff () [LOG]
setLogLvl : (l : LogLevel n) -> Eff () [LOG]

Set the logging level.

l

The new logging level.

logN : (l : Nat) -> {auto prf : LTE l (fromInteger 70)} -> (m : String) -> Eff () [LOG]

Log msg at the given level specified as a natural number.

l

The level to log.

m

The message to log.

log : (l : LogLevel n) -> (m : String) -> Eff () [LOG]

Log msg at the given level specified as a natural number.

l

The level to log.

m

The message to log.

info : String -> Eff () [LOG]
fatal : String -> Eff () [LOG]
error : String -> Eff () [LOG]
debug : String -> Eff () [LOG]
MkLogRes : (getLevel : LogLevel n) -> LogRes
data Logging : Effect

A Logging effect that displays a logging message to be logged at a
certain level.

SetLvl : (lvl : LogLevel n) -> sig Logging () LogRes LogRes

Change the logging level.

lvl

The new logging level.

Log : (lvl : LogLevel n) -> (msg : String) -> sig Logging () LogRes

Log a message.

lvl

The logging level it should appear at.

msg

The message to log.

record LogRes 

The resource that the log effect is defined over.

MkLogRes : (getLevel : LogLevel n) -> LogRes
getLevel : (rec : LogRes) -> LogLevel (free_n rec)
LOG : EFFECT

A Logging Effect.