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 AbsToCon

Defined in Agda.Syntax.Translation.AbstractToConcrete

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 (ChangeT 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