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.