Agda.Syntax.Builtin

This module defines the names of all BUILTINs.

Documentation

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

builtinSigma :: String

builtinBool :: String

builtinTrue :: String

builtinFalse :: String

builtinList :: String

builtinNil :: String

builtinCons :: String

builtinIO :: String

builtinMaybe :: String

builtinNothing :: String

builtinJust :: String

builtinPath :: String

builtinPathP :: String

builtinInterval :: String

builtinIZero :: String

builtinIOne :: String

builtinPartial :: String

builtinPartialP :: String

builtinIMin :: String

builtinIMax :: String

builtinINeg :: String

builtinIsOne :: String

builtinItIsOne :: String

builtinIsOne1 :: String

builtinIsOne2 :: String

builtinIsOneEmpty :: String

builtinComp :: String

builtinPOr :: String

builtinTrans :: String

builtinHComp :: String

builtinSub :: String

builtinSubIn :: String

builtinSubOut :: String

builtinEquiv :: String

builtinEquivFun :: String

builtinEquivProof :: String

builtinTranspProof :: String

builtinGlue :: String

builtin_glue :: String

builtin_unglue :: String

builtin_glueU :: String

builtin_unglueU :: String

builtinFaceForall :: String

builtinId :: String

builtinReflId :: String

builtinConId :: String

builtinIdElim :: 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

builtinSet :: String

builtinProp :: String

builtinSetOmega :: String

builtinStrictSet :: String

builtinSSetOmega :: String

builtinLockUniv :: String

builtinIntervalUniv :: String

builtinFromNat :: String

builtinFromNeg :: String

builtinFromString :: String

builtinQName :: String

builtinAgdaSort :: String

builtinAgdaSortSet :: String

builtinAgdaSortLit :: String

builtinAgdaSortProp :: String

builtinAgdaSortPropLit :: String

builtinAgdaSortInf :: String

builtinAgdaSortUnsupported :: String

builtinHiding :: String

builtinHidden :: String

builtinInstance :: String

builtinVisible :: String

builtinRelevance :: String

builtinRelevant :: String

builtinIrrelevant :: String

builtinQuantity :: String

builtinQuantity0 :: String

builtinQuantityω :: String

builtinModality :: String

builtinModalityConstructor :: String

builtinAssoc :: String

builtinAssocLeft :: String

builtinAssocRight :: String

builtinAssocNon :: String

builtinPrecedence :: String

builtinPrecRelated :: String

builtinPrecUnrelated :: String

builtinFixity :: String

builtinFixityFixity :: String

builtinArgInfo :: String

builtinArgArgInfo :: String

builtinArg :: 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

builtinAgdaErrorPartPatt :: 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

builtinAgdaTCMDeclareData :: String

builtinAgdaTCMDefineData :: String

builtinAgdaTCMDefineFun :: String

builtinAgdaTCMGetType :: String

builtinAgdaTCMGetDefinition :: String

builtinAgdaTCMQuoteTerm :: String

builtinAgdaTCMUnquoteTerm :: String

builtinAgdaTCMQuoteOmegaTerm :: String

builtinAgdaTCMBlockOnMeta :: String

builtinAgdaTCMCommit :: String

builtinAgdaTCMIsMacro :: String

builtinAgdaTCMFormatErrorParts :: String

builtinAgdaTCMDebugPrint :: String

builtinAgdaTCMWithNormalisation :: String

builtinAgdaTCMWithReconsParams :: String

builtinAgdaTCMOnlyReduceDefs :: String

builtinAgdaTCMDontReduceDefs :: String

builtinAgdaTCMNoConstraints :: String

builtinAgdaTCMRunSpeculative :: String

builtinAgdaTCMExec :: String

builtinAgdaTCMGetInstances :: String

isBuiltinNoDef :: String -> Bool

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.

{-# BUILTIN TYPE Type #-}

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

builtinsNoDef :: [String]

sizeBuiltins :: [String]