Constructors
Instances1MonadState
Monad m => MonadState FreshThings (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
ModuleAgda-2.7.0.1Haskell2010
Agda.TypeChecking.Conversion.Pure
- 2 types
- 4 values
- PackageAgda-2.7.0.1
- Exports6
- LanguageHaskell2010
- LicenceMIT
Constructors
Instances29MonadTrans, MonadError, MonadState, MonadFresh, Monad, Functor, …
MonadTrans PureConversionTDefined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadError TCErr (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadState FreshThings (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh NameId (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh ProblemId (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh Int (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => Monad (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureFunctor m => Functor (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonadFail m => MonadFail (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => Applicative (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureHasOptions m => HasOptions (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => MonadBlock (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonadReduce m => MonadReduce (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureReadTCState m => MonadStConcreteNames (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonadTCEnv m => MonadTCEnv (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureReadTCState m => ReadTCState (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureHasBuiltins m => HasBuiltins (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonadAddContext m => MonadAddContext (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonadDebug m => MonadDebug (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureHasConstInfo m => HasConstInfo (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureReadTCState m => MonadStatistics (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(IsString a, Monad m) => IsString (PureConversionT m a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure(Monad m, Semigroup a) => Semigroup (PureConversionT m a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.PureMonad m => Null (PureConversionT m Doc)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure