Agda.TypeChecking.Monad.Builtin

Documentation

class (Functor m, Applicative m, Monad m) => HasBuiltins m where

Minimal complete definition

getBuiltinThing

Methods

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

Instances

HasBuiltins ReduceM

Defined in Agda.TypeChecking.Reduce.Monad

Methods

getBuiltinThing :: String -> ReduceM (Maybe (Builtin PrimFun))

HasBuiltins m => HasBuiltins (MaybeT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> MaybeT m (Maybe (Builtin PrimFun))

MonadIO m => HasBuiltins (TCMT m)

Defined in Agda.TypeChecking.Monad.Builtin

Methods

getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun))

litType :: Literal -> TCM Type

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()

bindBuiltinName :: String -> Term -> TCM ()

bindPrimitive :: String -> PrimFun -> TCM ()

getBuiltin :: String -> TCM Term

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)

getPrimitive :: String -> TCM PrimFun

constructorForm :: Term -> TCM Term

Rewrite a literal to constructor form if possible.

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

The names of built-in things

primInteger :: TCM Term

primIntegerPos :: TCM Term

primIntegerNegSuc :: TCM Term

primFloat :: TCM Term

primChar :: TCM Term

primString :: TCM Term

primUnit :: TCM Term

primUnitUnit :: TCM Term

primBool :: TCM Term

primTrue :: TCM Term

primFalse :: TCM Term

primList :: TCM Term

primNil :: TCM Term

primCons :: TCM Term

primIO :: TCM Term

primNat :: TCM Term

primSuc :: TCM Term

primZero :: TCM Term

primNatPlus :: TCM Term

primNatMinus :: TCM Term

primNatTimes :: TCM Term

primNatDivSucAux :: TCM Term

primNatModSucAux :: TCM Term

primNatEquality :: TCM Term

primNatLess :: TCM Term

primWord64 :: TCM Term

primSizeUniv :: TCM Term

primSize :: TCM Term

primSizeLt :: TCM Term

primSizeSuc :: TCM Term

primSizeInf :: TCM Term

primSizeMax :: TCM Term

primInf :: TCM Term

primSharp :: TCM Term

primFlat :: TCM Term

primEquality :: TCM Term

primRefl :: TCM Term

primRewrite :: TCM Term

primLevel :: TCM Term

primLevelZero :: TCM Term

primLevelSuc :: TCM Term

primLevelMax :: TCM Term

primFromNat :: TCM Term

primFromNeg :: TCM Term

primFromString :: TCM Term

primQName :: TCM Term

primArgInfo :: TCM Term

primArgArgInfo :: TCM Term

primArg :: TCM Term

primArgArg :: TCM Term

primAbs :: TCM Term

primAbsAbs :: TCM Term

primAgdaTerm :: TCM Term

primAgdaTermVar :: TCM Term

primAgdaTermLam :: TCM Term

primAgdaTermExtLam :: TCM Term

primAgdaTermDef :: TCM Term

primAgdaTermCon :: TCM Term

primAgdaTermPi :: TCM Term

primAgdaTermSort :: TCM Term

primAgdaTermLit :: TCM Term

primAgdaTermUnsupported :: TCM Term

primAgdaTermMeta :: TCM Term

primAgdaErrorPart :: TCM Term

primAgdaErrorPartString :: TCM Term

primAgdaErrorPartTerm :: TCM Term

primAgdaErrorPartName :: TCM Term

primHiding :: TCM Term

primHidden :: TCM Term

primInstance :: TCM Term

primVisible :: TCM Term

primRelevance :: TCM Term

primRelevant :: TCM Term

primIrrelevant :: TCM Term

primAssoc :: TCM Term

primAssocLeft :: TCM Term

primAssocRight :: TCM Term

primAssocNon :: TCM Term

primPrecedence :: TCM Term

primPrecRelated :: TCM Term

primPrecUnrelated :: TCM Term

primFixity :: TCM Term

primFixityFixity :: TCM Term

primAgdaLiteral :: TCM Term

primAgdaLitNat :: TCM Term

primAgdaLitWord64 :: TCM Term

primAgdaLitFloat :: TCM Term

primAgdaLitString :: TCM Term

primAgdaLitChar :: TCM Term

primAgdaLitQName :: TCM Term

primAgdaLitMeta :: TCM Term

primAgdaSort :: TCM Term

primAgdaSortSet :: TCM Term

primAgdaSortLit :: TCM Term

primAgdaSortUnsupported :: TCM Term

primAgdaDefinition :: TCM Term

primAgdaDefinitionFunDef :: TCM Term

primAgdaDefinitionDataDef :: TCM Term

primAgdaDefinitionRecordDef :: TCM Term

primAgdaDefinitionPostulate :: TCM Term

primAgdaDefinitionPrimitive :: TCM Term

primAgdaDefinitionDataConstructor :: TCM Term

primAgdaClause :: TCM Term

primAgdaClauseClause :: TCM Term

primAgdaClauseAbsurd :: TCM Term

primAgdaPattern :: TCM Term

primAgdaPatCon :: TCM Term

primAgdaPatVar :: TCM Term

primAgdaPatDot :: TCM Term

primAgdaPatLit :: TCM Term

primAgdaPatProj :: TCM Term

primAgdaPatAbsurd :: TCM Term

primAgdaMeta :: TCM Term

primAgdaTCM :: TCM Term

primAgdaTCMReturn :: TCM Term

primAgdaTCMBind :: TCM Term

primAgdaTCMUnify :: TCM Term

primAgdaTCMTypeError :: TCM Term

primAgdaTCMInferType :: TCM Term

primAgdaTCMCheckType :: TCM Term

primAgdaTCMNormalise :: TCM Term

primAgdaTCMReduce :: TCM Term

primAgdaTCMCatchError :: TCM Term

primAgdaTCMGetContext :: TCM Term

primAgdaTCMExtendContext :: TCM Term

primAgdaTCMInContext :: TCM Term

primAgdaTCMFreshName :: TCM Term

primAgdaTCMDeclareDef :: TCM Term

primAgdaTCMDeclarePostulate :: TCM Term

primAgdaTCMDefineFun :: TCM Term

primAgdaTCMGetType :: TCM Term

primAgdaTCMGetDefinition :: TCM Term

primAgdaTCMQuoteTerm :: TCM Term

primAgdaTCMUnquoteTerm :: TCM Term

primAgdaTCMBlockOnMeta :: TCM Term

primAgdaTCMCommit :: TCM Term

primAgdaTCMIsMacro :: TCM Term

primAgdaTCMWithNormalisation :: TCM Term

primAgdaTCMDebugPrint :: TCM Term

builtinNat :: String

builtinSuc :: String

builtinZero :: String

builtinNatPlus :: String

builtinNatMinus :: String

builtinNatTimes :: String

builtinNatDivSucAux :: String

builtinNatModSucAux :: String

builtinNatEquals :: String

builtinNatLess :: String

builtinInteger :: String

builtinIntegerPos :: String

builtinIntegerNegSuc :: String

builtinWord64 :: String

builtinFloat :: String

builtinChar :: String

builtinString :: String

builtinUnit :: String

builtinUnitUnit :: String

builtinBool :: String

builtinTrue :: String

builtinFalse :: String

builtinList :: String

builtinNil :: String

builtinCons :: String

builtinIO :: String

builtinSizeUniv :: String

builtinSize :: String

builtinSizeLt :: String

builtinSizeSuc :: String

builtinSizeInf :: String

builtinSizeMax :: String

builtinInf :: String

builtinSharp :: String

builtinFlat :: String

builtinEquality :: String

builtinRefl :: String

builtinRewrite :: String

builtinLevelMax :: String

builtinLevel :: String

builtinLevelZero :: String

builtinLevelSuc :: String

builtinFromNat :: String

builtinFromNeg :: String

builtinFromString :: String

builtinQName :: String

builtinAgdaSort :: String

builtinAgdaSortSet :: String

builtinAgdaSortLit :: String

builtinAgdaSortUnsupported :: String

builtinHiding :: String

builtinHidden :: String

builtinInstance :: String

builtinVisible :: String

builtinRelevance :: String

builtinRelevant :: String

builtinIrrelevant :: String

builtinArg :: String

builtinAssoc :: String

builtinAssocLeft :: String

builtinAssocRight :: String

builtinAssocNon :: String

builtinPrecedence :: String

builtinPrecRelated :: String

builtinPrecUnrelated :: String

builtinFixity :: String

builtinFixityFixity :: String

builtinArgInfo :: String

builtinArgArgInfo :: String

builtinArgArg :: String

builtinAbs :: String

builtinAbsAbs :: String

builtinAgdaTerm :: String

builtinAgdaTermVar :: String

builtinAgdaTermLam :: String

builtinAgdaTermExtLam :: String

builtinAgdaTermDef :: String

builtinAgdaTermCon :: String

builtinAgdaTermPi :: String

builtinAgdaTermSort :: String

builtinAgdaTermLit :: String

builtinAgdaTermUnsupported :: String

builtinAgdaTermMeta :: String

builtinAgdaErrorPart :: String

builtinAgdaErrorPartString :: String

builtinAgdaErrorPartTerm :: String

builtinAgdaErrorPartName :: String

builtinAgdaLiteral :: String

builtinAgdaLitNat :: String

builtinAgdaLitWord64 :: String

builtinAgdaLitFloat :: String

builtinAgdaLitChar :: String

builtinAgdaLitString :: String

builtinAgdaLitQName :: String

builtinAgdaLitMeta :: String

builtinAgdaClause :: String

builtinAgdaClauseClause :: String

builtinAgdaClauseAbsurd :: String

builtinAgdaPattern :: String

builtinAgdaPatVar :: String

builtinAgdaPatCon :: String

builtinAgdaPatDot :: String

builtinAgdaPatLit :: String

builtinAgdaPatProj :: String

builtinAgdaPatAbsurd :: String

builtinAgdaDefinitionFunDef :: String

builtinAgdaDefinitionDataDef :: String

builtinAgdaDefinitionRecordDef :: String

builtinAgdaDefinitionDataConstructor :: String

builtinAgdaDefinitionPostulate :: String

builtinAgdaDefinitionPrimitive :: String

builtinAgdaDefinition :: String

builtinAgdaMeta :: String

builtinAgdaTCM :: String

builtinAgdaTCMReturn :: String

builtinAgdaTCMBind :: String

builtinAgdaTCMUnify :: String

builtinAgdaTCMTypeError :: String

builtinAgdaTCMInferType :: String

builtinAgdaTCMCheckType :: String

builtinAgdaTCMNormalise :: String

builtinAgdaTCMReduce :: String

builtinAgdaTCMCatchError :: String

builtinAgdaTCMGetContext :: String

builtinAgdaTCMExtendContext :: String

builtinAgdaTCMInContext :: String

builtinAgdaTCMFreshName :: String

builtinAgdaTCMDeclareDef :: String

builtinAgdaTCMDeclarePostulate :: String

builtinAgdaTCMDefineFun :: String

builtinAgdaTCMGetType :: String

builtinAgdaTCMGetDefinition :: String

builtinAgdaTCMQuoteTerm :: String

builtinAgdaTCMUnquoteTerm :: String

builtinAgdaTCMBlockOnMeta :: String

builtinAgdaTCMCommit :: String

builtinAgdaTCMIsMacro :: String

builtinAgdaTCMWithNormalisation :: String

builtinAgdaTCMDebugPrint :: String

builtinsNoDef :: [String]

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{--}

The type of Type would be Type : Level → Setω which is not valid Agda.

data CoinductionKit

The coinductive primitives.

Constructors

CoinductionKit

Fields

• nameOfInf :: QName
• nameOfSharp :: QName
• nameOfFlat :: QName

coinductionKit' :: TCM CoinductionKit

Tries to build a CoinductionKit.

coinductionKit :: TCM (Maybe CoinductionKit)

Builtin equality

primEqualityName :: TCM QName

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView

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

Precondition: type is reduced.

equalityUnview :: EqualityView -> Type

Revert the EqualityView.

Postcondition: type is reduced.