| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Reduce.Monad
Contents
Synopsis
- constructorForm :: Term -> ReduceM Term
- enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b
- underAbstraction_ :: Subst t a => Abs a -> (a -> ReduceM b) -> ReduceM b
- getConstInfo :: HasConstInfo m => QName -> m Definition
- isInstantiatedMeta :: MetaId -> ReduceM Bool
- lookupMeta :: MetaId -> ReduceM MetaVariable
- askR :: ReduceM ReduceEnv
- applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (m a -> m a) -> m a -> m a
Documentation
constructorForm :: Term -> ReduceM Term #
enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b #
getConstInfo :: HasConstInfo m => QName -> m Definition #
Lookup the definition of a name. The result is a closed thing, all free variables have been abstracted over.
isInstantiatedMeta :: MetaId -> ReduceM Bool #
lookupMeta :: MetaId -> ReduceM MetaVariable #
applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (m a -> m a) -> m a -> m a #
Apply a function if a certain verbosity level is activated.
Precondition: The level must be non-negative.
Orphan instances
| HasOptions ReduceM # | |
| MonadDebug ReduceM # | |
Methods displayDebugMessage :: Int -> String -> ReduceM () # traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String # | |
| HasBuiltins ReduceM # | |
| HasConstInfo ReduceM # | |
Methods getConstInfo :: QName -> ReduceM Definition # getConstInfo' :: QName -> ReduceM (Either SigError Definition) # | |