Agda-2.4.2.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell98

Agda.TypeChecking.Monad.Trace

Contents

Synopsis

Trace

traceCallM :: MonadTCM tcm => tcm (Maybe r -> Call) -> tcm a -> tcm a Source

traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm a -> tcm a Source

Record a function call in the trace.

traceCall_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm r -> tcm r Source

traceCallCPS :: MonadTCM tcm => (Maybe r -> Call) -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b Source

traceCallCPS_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm a -> (tcm a -> tcm b) -> tcm b Source