Agda.TypeChecking.Monad.Builtin · Agda-2.7.0.1

classclass (Functor m, Applicative m, MonadFail m) => HasBuiltins (m :: Type -> Type) where

#

Methods

getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))

Instances17HasBuiltins, …

HasBuiltins AbsToConDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.AbstractToConcrete
HasBuiltins TerMDefined in Agda-2.7.0.1 · Agda.Termination.Monad
HasBuiltins ReduceMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce.Monad · orphan
HasBuiltins BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins NLMDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rewriting.NonLinMatch
HasBuiltins m => HasBuiltins (PureConversionT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Conversion.Pure
HasBuiltins m => HasBuiltins (BlockT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (NamesT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Names
HasBuiltins m => HasBuiltins (ListT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ChangeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (MaybeT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
MonadIO m => HasBuiltins (TCMT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ExceptT e m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (IdentityT m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (ReaderT e m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins m => HasBuiltins (StateT s m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin

valuegetBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName)

#

valueconstructorForm :: HasBuiltins m => Term -> m Term

#

Rewrite a literal to constructor form if possible.

valuegetName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName)

#

valuegetBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)

#

valueprimConId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIdElim :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIMin :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimINeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPartial :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPartialP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSubOut :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimGlue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFaceForall :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimHComp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatPlus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatMinus :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatTimes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatDivSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatModSucAux :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNatLess :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLevelZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLevelSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLevelMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLockUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

newtypenewtype BuiltinAccess a

#

The trivial implementation of HasBuiltins, using a constant TCState.

This may be used instead of TCMT/ReduceM where builtins must be accessed in a pure context.

Constructors

BuiltinAccess
- unBuiltinAccess :: TCState -> a

Instances5Monad, Functor, MonadFail, Applicative, HasBuiltins

Monad BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
Functor BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
MonadFail BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
Applicative BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
HasBuiltins BuiltinAccessDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin

valuerunBuiltinAccess :: TCState -> BuiltinAccess a -> a

#

Run a BuiltinAccess monad.

valuelitType

:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> Literal
-> m Type

#

valueprimZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valuesetBuiltinThings :: BuiltinThings PrimFun -> TCM ()

#

valuebindBuiltinName :: BuiltinId -> Term -> TCM ()

#

valuebindPrimitive :: PrimitiveId -> PrimFun -> TCM ()

#

valuebindBuiltinRewriteRelation :: QName -> TCM ()

#

Add one (more) relation symbol to the rewrite relations.

valuegetBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName)

#

Get the currently registered rewrite relation symbols.

valuegetBuiltinRewriteRelations' :: HasBuiltins m => m (Maybe (Set QName))

#

Get the currently registered rewrite relation symbols, if any.

valuegetBuiltin :: (HasBuiltins m, MonadTCError m) => BuiltinId -> m Term

#

valuegetPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)

#

valuegetPrimitive

:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> PrimitiveId
-> m PrimFun

#

valuegetPrimitiveTerm

:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> PrimitiveId
-> m Term

#

valuegetPrimitiveTerm' :: HasBuiltins m => PrimitiveId -> m (Maybe Term)

#

valuegetPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName)

#

valuegetTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term)

#

valuegetTerm :: (HasBuiltins m, IsBuiltin a) => String -> a -> m Term

#

getTerm use name looks up name as a primitive or builtin, and throws an error otherwise. The use argument describes how the name is used for the sake of the error message.

valueconstructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term

#

valueprimInteger :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIntegerPos :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIntegerNegSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimUnitUnit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimBool :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimTrue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFalse :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSigma :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimList :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNil :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimCons :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIO :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimMaybe :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimNothing :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimJust :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPath :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPathP :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIntervalUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimInterval :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIZero :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimItIsOne :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIsOne1 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIsOne2 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIsOneEmpty :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSub :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSubIn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimTrans :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimId :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimEquiv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimEquivFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimEquivProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimTranspProof :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprim_glue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprim_unglue :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprim_glueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprim_unglueU :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSizeUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSize :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSizeLt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSizeSuc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSizeInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSizeMax :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSharp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFlat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimEquality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimRefl :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLevel :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimLevelUniv :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimStrictSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPropOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimSSetOmega :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFromNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFromNeg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFromString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimArgArgInfo :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimArgArg :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAbsAbs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermExtLam :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermPi :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTermMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaErrorPart :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaErrorPartString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaErrorPartTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaErrorPartPatt :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaErrorPartName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimHiding :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimHidden :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimInstance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimVisible :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimRelevance :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimRelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimIrrelevant :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimQuantity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimQuantity0 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimQuantityω :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimModality :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimModalityConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAssoc :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAssocLeft :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAssocRight :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAssocNon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPrecedence :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPrecRelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimPrecUnrelated :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimFixityFixity :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLiteral :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitNat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitWord64 :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitFloat :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitString :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitChar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitQName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaLitMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSort :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortSet :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortProp :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortPropLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortInf :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaSortUnsupported :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionFunDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionDataDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionRecordDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionPostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaDefinitionDataConstructor :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaClauseClause :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaClauseAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPattern :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatCon :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatDot :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatLit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatProj :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaPatAbsurd :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaBlocker :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaBlockerAny :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaBlockerAll :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaBlockerMeta :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCM :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMReturn :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMBind :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMUnify :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMTypeError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMInferType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMCheckType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMNormalise :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMReduce :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMCatchError :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMGetContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMExtendContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMInContext :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMFreshName :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDeclareDef :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDeclarePostulate :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDeclareData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDefineData :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDefineFun :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMGetType :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMGetDefinition :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMQuoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMUnquoteTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMQuoteOmegaTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMCommit :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMIsMacro :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMBlock :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMFormatErrorParts :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMDebugPrint :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMWithNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMWithReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMWithExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMWithReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMAskNormalisation :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMAskReconstructed :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMAskExpandLast :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMAskReduceDefs :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMNoConstraints :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMWorkOnTypes :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMRunSpeculative :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMExec :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMGetInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMSolveInstances :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMPragmaForeign :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

valueprimAgdaTCMPragmaCompile :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

#

datadata CoinductionKit

#

The coinductive primitives.

Constructors

CoinductionKit
- nameOfInf :: QName
- nameOfSharp :: QName
- nameOfFlat :: QName

valuecoinductionKit' :: TCM CoinductionKit

#

Tries to build a CoinductionKit.

valuecoinductionKit :: TCM (Maybe CoinductionKit)

#

datadata SortKit

#

Sort primitives.

Constructors

SortKit
- nameOfUniv :: UnivSize -> Univ -> QName
- isNameOfUniv :: QName -> Maybe (UnivSize, Univ)

valuemkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit

#

valuesortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit

#

Compute a SortKit in an environment that supports failures.

When optLoadPrimitives is set to False, sortKit is a fallible operation, so for the uses of sortKit in fallible contexts (e.g. TCM), we report a type error rather than exploding.

valueinfallibleSortKit :: HasBuiltins m => m SortKit

#

Compute a SortKit in contexts that do not support failure (e.g. Reify). This should only be used when we are sure that the primitive sorts have been bound, i.e. because it is "after" type checking.

valuegetPrimName :: Term -> QName

#

valueisPrimitive :: HasBuiltins m => PrimitiveId -> QName -> m Bool

#

valueintervalSort :: Sort

#

valueintervalView' :: HasBuiltins m => m (Term -> IntervalView)

#

valueintervalView :: HasBuiltins m => Term -> m IntervalView

#

valueintervalUnview :: HasBuiltins m => IntervalView -> m Term

#

valueintervalUnview' :: HasBuiltins m => m (IntervalView -> Term)

#

valuepathView :: HasBuiltins m => Type -> m PathView

#

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

valuepathView' :: HasBuiltins m => m (Type -> PathView)

#

valueidViewAsPath :: HasBuiltins m => Type -> m PathView

#

Non dependent Path

valueboldPathView :: Type -> PathView

#

valuepathUnview :: PathView -> Type

#

Revert the PathView.

Postcondition: type is reduced.

valueconidView' :: HasBuiltins m => m (Term -> Term -> Maybe (Arg Term, Arg Term))

#

valueprimEqualityName :: TCM QName

#

Get the name of the equality type.

valueequalityView :: Type -> TCM EqualityView

#

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

classclass EqualityUnview a where

#

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type

Instances2EqualityUnview

EqualityUnview EqualityTypeDataDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin
EqualityUnview EqualityViewDefined in Agda-2.7.0.1 · Agda.TypeChecking.Monad.Builtin

valueconstrainedPrims :: [PrimitiveId]

#

Primitives with typechecking constrants.

valuegetNameOfConstrained :: HasBuiltins m => PrimitiveId -> m (Maybe QName)

#