| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce.Monad
Contents
Synopsis
- constructorForm :: HasBuiltins m => Term -> m Term
- enterClosure :: LensClosure a c => c -> (a -> ReduceM b) -> ReduceM b
- getConstInfo :: HasConstInfo m => QName -> m Definition
- askR :: ReduceM ReduceEnv
- applyWhenVerboseS :: MonadDebug m => VerboseKey -> VerboseLevel -> (m a -> m a) -> m a -> m a
Documentation
constructorForm :: HasBuiltins m => Term -> m Term Source #
enterClosure :: LensClosure a c => c -> (a -> ReduceM b) -> ReduceM 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.