Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Conversion.Pure

Documentation

data FreshThings Source #

Constructors

FreshThings 

Instances

Instances details
Monad m => MonadState FreshThings (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

newtype PureConversionT (m :: Type -> Type) a Source #

Constructors

PureConversionT 

Fields

Instances

Instances details
MonadTrans PureConversionT Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

lift :: Monad m => m a -> PureConversionT m a

Monad m => MonadFresh NameId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => MonadFresh ProblemId (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => MonadFresh Int (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fresh :: PureConversionT m Int Source #

Monad m => MonadError TCErr (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => MonadState FreshThings (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasOptions m => HasOptions (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => MonadBlock (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadReduce m => MonadReduce (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

ReadTCState m => ReadTCState (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(PureTCM m, MonadBlock m) => MonadConstraint (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadAddContext m => MonadAddContext (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadDebug m => MonadDebug (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(PureTCM m, MonadBlock m) => MonadInteractionPoints (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(PureTCM m, MonadBlock m) => MonadMetaSolver (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasConstInfo m => HasConstInfo (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

ReadTCState m => MonadStatistics (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

modifyCounter :: String -> (Integer -> Integer) -> PureConversionT m () Source #

(PureTCM m, MonadBlock m) => MonadWarning (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Monad m => Applicative (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Functor m => Functor (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b

(<$) :: a -> PureConversionT m b -> PureConversionT m a #

Monad m => Monad (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

MonadFail m => MonadFail (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fail :: String -> PureConversionT m a

Monad m => Null (PureConversionT m Doc) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(Monad m, Semigroup a) => Semigroup (PureConversionT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

(IsString a, Monad m) => IsString (PureConversionT m a) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

fromString :: String -> PureConversionT m a

pureEqualTerm :: (PureTCM m, MonadBlock m) => Type -> Term -> Term -> m Bool Source #

pureEqualType :: (PureTCM m, MonadBlock m) => Type -> Type -> m Bool Source #