Constructors
Instances1MonadState
Monad m => MonadState FreshThings (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.Conversion.Pure
Synopsis
- data FreshThings
- newtype PureConversionT
- value pureEqualTerm
- value pureEqualTermB
- value pureEqualType
- value pureEqualTypeB
- value pureCompareAs
- value runPureConversion
- value runPureConversionB
- PackageAgda-2.8.0.2
- Exports9
- LanguageHaskell2010
- LicenceMIT
- SourcePure.hs
Constructors
Instances29MonadTrans, MonadError, MonadState, MonadFresh, Monad, Functor, …
MonadTrans PureConversionTDefined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadError TCErr (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadState FreshThings (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh NameId (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh ProblemId (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadFresh Int (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => Monad (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureFunctor m => Functor (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadFail m => MonadFail (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => Applicative (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureHasOptions m => HasOptions (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => MonadBlock (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadReduce m => MonadReduce (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureReadTCState m => MonadStConcreteNames (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadTCEnv m => MonadTCEnv (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureReadTCState m => ReadTCState (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureHasBuiltins m => HasBuiltins (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PurePureTCM m => MonadConstraint (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadAddContext m => MonadAddContext (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonadDebug m => MonadDebug (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PurePureTCM m => MonadInteractionPoints (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PurePureTCM m => MonadMetaSolver (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureHasConstInfo m => HasConstInfo (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureReadTCState m => MonadStatistics (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PurePureTCM m => MonadWarning (PureConversionT m)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure(IsString a, Monad m) => IsString (PureConversionT m a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure(Monad m, Semigroup a) => Semigroup (PureConversionT m a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.PureMonad m => Null (PureConversionT m Doc)Defined in Agda-2.8.0.2 · Agda.TypeChecking.Conversion.Pure
Return the blocker instead of throwing a patternViolation.
Return the blocker instead of throwing a patternViolation.