Agda.TypeChecking.Monad.Pure

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

Instances

PureTCM TerM

Defined in Agda.Termination.Monad

PureTCM ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

PureTCM TCM

Defined in Agda.TypeChecking.Monad.Pure

PureTCM NLM

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m)

Defined in Agda.TypeChecking.Conversion.Pure

PureTCM m => PureTCM (BlockT m)

Defined in Agda.TypeChecking.Monad.Pure

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m)

Defined in Agda.TypeChecking.Names

PureTCM m => PureTCM (ListT m)

Defined in Agda.TypeChecking.Monad.Pure

PureTCM m => PureTCM (MaybeT m)

Defined in Agda.TypeChecking.Monad.Pure

PureTCM m => PureTCM (ExceptT e m)

Defined in Agda.TypeChecking.Monad.Pure

PureTCM m => PureTCM (IdentityT m)

Defined in Agda.TypeChecking.Monad.Pure

PureTCM m => PureTCM (ReaderT r m)

Defined in Agda.TypeChecking.Monad.Pure

PureTCM m => PureTCM (StateT s m)

Defined in Agda.TypeChecking.Monad.Pure

(PureTCM m, Monoid w) => PureTCM (WriterT w m)

Defined in Agda.TypeChecking.Monad.Pure