class
class (HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadDebug m, MonadReduce m, MonadTCEnv m, ReadTCState m) => PureTCM (m :: Type -> Type)Instances16PureTCM, …
PureTCM TerMDefined in Agda-2.8.0.2 · Agda.Termination.MonadPureTCM ReduceMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Reduce.Monad · orphanPureTCM TCMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM NLMDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rewriting.NonLinMatchPureTCM m => PureTCM (BlockT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (ListT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (ChangeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (MaybeT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Pure(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (AbsToConT m)Defined in Agda-2.8.0.2 · Agda.Syntax.Translation.AbstractToConcrete(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (NamesT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.NamesPureTCM m => PureTCM (ExceptT e m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (IdentityT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (ReaderT r m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.PurePureTCM m => PureTCM (StateT s m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Pure(PureTCM m, Monoid w) => PureTCM (WriterT w m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Monad.Pure