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

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.TypeChecking.Monad.Pure

Description

A typeclass collecting all `pure` typechecking operations | (i.e. ones that do not modify the typechecking state, throw or | catch errors, or do IO other than debug printing).

# Documentation

class (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadTCEnv m, ReadTCState m) => PureTCM m Source #

#### Instances

Instances details

PureTCM TerM Source # |
Instance details Defined in Agda.Termination.Monad
PureTCM ReduceM Source # |
Instance details Defined in Agda.TypeChecking.Reduce.Monad
PureTCM TCM Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM NLM Source # |
Instance details Defined in Agda.TypeChecking.Rewriting.NonLinMatch
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure
PureTCM m => PureTCM (BlockT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m) Source # |
Instance details Defined in Agda.TypeChecking.Names
PureTCM m => PureTCM (ListT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM m => PureTCM (MaybeT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM m => PureTCM (ExceptT e m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM m => PureTCM (IdentityT m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM m => PureTCM (ReaderT r m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
PureTCM m => PureTCM (StateT s m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure
(PureTCM m, Monoid w) => PureTCM (WriterT w m) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Pure