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