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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Reduce.Monad

Contents

- Orphan instances

Synopsis

- 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
- 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 :: HasBuiltins m => Term -> m Term Source #

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

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

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

addCtxTel :: MonadReduce m => Telescope -> m a -> m a 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.

isInstantiatedMeta :: MetaId -> ReduceM Bool Source #

lookupMeta :: MetaId -> ReduceM MetaVariable Source #

askR :: ReduceM ReduceEnv Source #

applyWhenVerboseS :: HasOptions m => VerboseKey -> Int -> (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.

# Orphan instances

MonadDebug ReduceM Source # |
Instance details Methods displayDebugMessage :: Int -> String -> ReduceM () Source # traceDebugMessage :: Int -> String -> ReduceM a -> ReduceM a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ReduceM String Source #
HasConstInfo ReduceM Source # |
Instance details Methods getConstInfo :: QName -> ReduceM Definition Source # getConstInfo' :: QName -> ReduceM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ReduceM RewriteRules Source #
HasBuiltins ReduceM Source # |
Instance details Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #