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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Monad.Trace

Contents

- Trace

Synopsis

- 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
- getCurrentRange :: (MonadTCM tcm, MonadDebug tcm) => tcm Range
- setCurrentRange :: (MonadTCM tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a

# Trace

interestingCall :: Closure Call -> Bool Source #

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

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

Record a function call in the trace.

getCurrentRange :: (MonadTCM tcm, MonadDebug tcm) => tcm Range Source #

setCurrentRange :: (MonadTCM tcm, MonadDebug tcm, HasRange x) => x -> tcm a -> tcm a Source #

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`).