Agda-2.6.2.1.20220320: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

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