Idris2Doc : Core.Context.Log

Core.Context.Log

(source)
Reexports
import public Core.Context
Definitions
logString : String -> Nat -> String -> Core ()
  Visibility: export
logString' : LogLevel -> String -> Core ()
  Visibility: export
logging' : Ref Ctxt Defs => LogLevel -> Core Bool
  Visibility: export
unverifiedLogging : Ref Ctxt Defs => String -> Nat -> Core Bool
  Visibility: export
logging : Ref Ctxt Defs => LogTopic -> Nat -> Core Bool
  Visibility: export
logTerm : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Term vars -> Core ()
  Log message with a term, translating back to human readable names first.

  Visibility: export
log' : Ref Ctxt Defs => LogLevel -> Lazy String -> Core ()
  Visibility: export
log : Ref Ctxt Defs => LogTopic -> Nat -> Lazy String -> Core ()
  Log a message with the given log level. Use increasingly
  high log level numbers for more granular logging.
  
  If you want to use some `Core` computation to produce a message string, use `logC`.
  I.e. instead of `log "topic" 10 "message \{show !(toFullNames fn)}"` use
  `logC "topic" 10 $ do pure ""message \{show !(toFullNames fn)}""`.
  This will enfore that additional computation happends only when needed.
  `do` before `pure` in this case ensures the correct bounds.

  Visibility: export
unverifiedLogC : Ref Ctxt Defs => String -> Nat -> Core String -> Core ()
  Visibility: export
logC : Ref Ctxt Defs => LogTopic -> Nat -> Core String -> Core ()
  Visibility: export
logTimeOver : Integer -> Core String -> Core a -> Core a
  Visibility: export
logTimeWhen : Ref Ctxt Defs => Bool -> Nat -> Lazy String -> Core a -> Core a
  Visibility: export
logTimeRecord : Ref Ctxt Defs => String -> Core a -> Core a
  Visibility: export
showTimeRecord : Ref Ctxt Defs => Core ()
  Visibility: export
logTime : Ref Ctxt Defs => Nat -> Lazy String -> Core a -> Core a
  Visibility: export