Agda.TypeChecking.Reduce.Monad

Documentation

constructorForm :: HasBuiltins m => Term -> m Term

enterClosure :: Closure a -> (a -> ReduceM b) -> ReduceM b

underAbstraction :: (MonadReduce m, Subst t a) => Dom Type -> Abs a -> (a -> m b) -> m b

underAbstraction_ :: (MonadReduce m, Subst t a) => Abs a -> (a -> m b) -> m b

addCtxTel :: MonadReduce m => Telescope -> m a -> m a

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

askR :: ReduceM ReduceEnv

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

MonadDebug ReduceM

Methods

displayDebugMessage :: Int -> String -> ReduceM ()

traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a

formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String

HasConstInfo ReduceM

Methods

getConstInfo :: QName -> ReduceM Definition

getConstInfo' :: QName -> ReduceM (Either SigError Definition)

getRewriteRulesFor :: QName -> ReduceM RewriteRules

HasBuiltins ReduceM

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun))