| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.TypeChecking.Monad.Trace

Contents

Trace

Synopsis

traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm r -> tcm r
traceCall_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm r -> tcm r
traceCallCPS :: MonadTCM tcm => (Maybe r -> Call) -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b
traceCallCPS_ :: MonadTCM tcm => (Maybe () -> Call) -> tcm a -> (tcm a -> tcm b) -> tcm b
getTrace :: MonadTCM tcm => tcm CallTrace
setTrace :: MonadTCM tcm => CallTrace -> tcm ()
getCurrentRange :: MonadTCM tcm => tcm Range
setCurrentRange :: MonadTCM tcm => Range -> tcm a -> tcm a
onTrace :: MonadTCM tcm => (CallTrace -> CallTrace) -> tcm ()
withTrace :: MonadTCM tcm => CallTrace -> tcm a -> tcm a

Trace

traceCall :: MonadTCM tcm => (Maybe r -> Call) -> tcm r -> tcm r | 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

getTrace :: MonadTCM tcm => tcm CallTrace | Source

setTrace :: MonadTCM tcm => CallTrace -> tcm () | Source

getCurrentRange :: MonadTCM tcm => tcm Range | Source

setCurrentRange :: MonadTCM tcm => Range -> tcm a -> tcm a | Source

onTrace :: MonadTCM tcm => (CallTrace -> CallTrace) -> tcm () | Source

withTrace :: MonadTCM tcm => CallTrace -> tcm a -> tcm a | Source

Produced by Haddock version 2.4.2