Agda.TypeChecking.Monad.Trace

Trace

interestingCall :: Closure Call -> Bool

traceCallM :: (MonadTCM tcm, MonadDebug tcm) => tcm Call -> tcm a -> tcm a

traceCall :: (MonadTCM tcm, MonadDebug tcm) => Call -> tcm a -> tcm a

Record a function call in the trace.

traceCallCPS :: (MonadTCM tcm, MonadDebug tcm) => Call -> (r -> tcm a) -> ((r -> tcm a) -> tcm b) -> tcm b

traceCallCPS_ :: (MonadTCM tcm, MonadDebug tcm) => Call -> tcm a -> (tcm a -> tcm b) -> tcm b

getCurrentRange :: TCM Range

setCurrentRange :: HasRange x => x -> TCM a -> TCM a

Sets the current range (for error messages etc.) to the range of the given object, if it has a range (i.e., its range is not noRange).