Language.Reflection.Logging

Reexports

Definitions

interface LogPosition : Type -> Type

Parameters: a
Methods:

logPosition : a -> String

Implementations:

LogPosition Con

LogPosition TypeInfo

logPosition : LogPosition a => a -> String

Totality: total
Visibility: public export

data LogPositions : Type

Totality: total
Visibility: public export
Constructors:

Nil : LogPositions

(::) : LogPosition a => a -> LogPositions -> LogPositions

Hint: 

Interpolation LogPositions

length : LogPositions -> Nat

Totality: total
Visibility: export

data LogLevel : Type

Totality: total
Visibility: public export
Constructors:

Warning : LogLevel

Info : LogLevel

Details : LogLevel

FineDetails : LogLevel

Trace : LogLevel

DetailedTrace : LogLevel

Debug : LogLevel

DetailedDebug : LogLevel

interface ElabLogLevels : Type

Methods:

toNatLevel : LogLevel -> Nat

defaultLogLevel : LogLevel

toNatLevel : ElabLogLevels => LogLevel -> Nat

Totality: total
Visibility: public export

defaultLogLevel : ElabLogLevels => LogLevel

Totality: total
Visibility: public export

DefaultElabLogLevels : ElabLogLevels

Totality: total
Visibility: public export

interface MonadLog : (Type -> Type) -> Type

Parameters: m
Constraints: Monad m
Constructor: 

MkMonadLog

Methods:

logPoint : ElabLogLevels => LogLevel -> (topic : String) -> So (topic /= fromString "") => LogPositions -> String -> m ()

logPoint : MonadLog m => ElabLogLevels => LogLevel -> (topic : String) -> So (topic /= fromString "") => LogPositions -> String -> m ()

Totality: total
Visibility: public export

logPoint' : MonadLog m => ElabLogLevels => (topic : String) -> So (topic /= fromString "") => LogPositions -> String -> m ()

Totality: total
Visibility: export

withLogPoint : MonadLog m => ElabLogLevels => LogLevel -> (topic : String) -> So (topic /= fromString "") => LogPositions -> String -> m a -> m a

Totality: total
Visibility: export

logValue : MonadLog m => ElabLogLevels => LogLevel -> (topic : String) -> So (topic /= fromString "") => LogPositions -> String -> a -> m a

Totality: total
Visibility: export

logBounds : MonadLog m => ElabLogLevels => LogLevel -> (topic : String) -> So (topic /= fromString "") => LogPositions -> m a -> m a

Totality: total
Visibility: export

logBounds' : MonadLog m => ElabLogLevels => (topic : String) -> So (topic /= fromString "") => LogPositions -> m a -> m a

Totality: total
Visibility: export

DefaultLog : Elaboration m => MonadLog m

Totality: total
Visibility: export