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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Reduce.Monad

Contents

- Orphan instances

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.

askR :: ReduceM ReduceEnv Source #

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.

# Orphan instances

HasBuiltins ReduceM Source # |
Instance details Methods getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun)) Source #
MonadAddContext ReduceM Source # |
Instance details Methods addCtx :: Name -> Dom Type -> ReduceM a -> ReduceM a Source # addLetBinding' :: Name -> Term -> Dom Type -> ReduceM a -> ReduceM a Source # updateContext :: Substitution -> (Context -> Context) -> ReduceM a -> ReduceM a Source # withFreshName :: Range -> ArgName -> (Name -> ReduceM a) -> ReduceM a Source #
MonadDebug ReduceM Source # |

Instance details

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> ReduceM String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> ReduceM a -> ReduceM a Source #

getVerbosity :: ReduceM Verbosity Source #

isDebugPrinting :: ReduceM Bool Source #

nowDebugPrinting :: ReduceM a -> ReduceM a Source #

PureTCM ReduceM Source # |
Instance details
HasConstInfo ReduceM Source # |
Instance details Methods getConstInfo :: QName -> ReduceM Definition Source # getConstInfo' :: QName -> ReduceM (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ReduceM RewriteRules Source #