| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce.Monad
Contents
Synopsis
- enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure c a) => c -> (a -> m b) -> m b
- getConstInfo :: HasConstInfo m => QName -> m Definition
- askR :: ReduceM ReduceEnv
- applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
Documentation
enterClosure :: (MonadTCEnv m, ReadTCState m, LensClosure c a) => c -> (a -> m b) -> m b Source #
getConstInfo :: HasConstInfo m => QName -> m Definition Source #
Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.
applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a Source #
Apply a function if a certain verbosity level is activated.
Precondition: The level must be non-negative.