    -- | This module defines the names of all BUILTINs.
    module Agda.Syntax.Builtin where

    import Agda.Utils.List

    builtinNat, builtinSuc, builtinZero, builtinNatPlus, builtinNatMinus,
      builtinNatTimes, builtinNatDivSucAux, builtinNatModSucAux, builtinNatEquals,
      builtinNatLess, builtinInteger, builtinIntegerPos, builtinIntegerNegSuc,
      builtinWord64,
      builtinFloat, builtinChar, builtinString, builtinUnit, builtinUnitUnit,
      builtinSigma,
      builtinBool, builtinTrue, builtinFalse,
      builtinList, builtinNil, builtinCons, builtinIO,
      builtinMaybe, builtinNothing, builtinJust,
      builtinPath, builtinPathP, builtinInterval, builtinIZero, builtinIOne, builtinPartial, builtinPartialP,
      builtinIMin, builtinIMax, builtinINeg,
      builtinIsOne,  builtinItIsOne, builtinIsOne1, builtinIsOne2, builtinIsOneEmpty,
      builtinComp, builtinPOr,
      builtinTrans, builtinHComp,
      builtinSub, builtinSubIn, builtinSubOut,
      builtinEquiv, builtinEquivFun, builtinEquivProof,
      builtinTranspProof,
      builtinGlue, builtin_glue, builtin_unglue,
      builtin_glueU, builtin_unglueU,
      builtinFaceForall,
      builtinId, builtinConId, builtinIdElim,
      builtinSizeUniv, builtinSize, builtinSizeLt,
      builtinSizeSuc, builtinSizeInf, builtinSizeMax,
      builtinInf, builtinSharp, builtinFlat,
      builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
      builtinLevel, builtinLevelZero, builtinLevelSuc,
      builtinSet, builtinProp, builtinSetOmega, builtinStrictSet, builtinSSetOmega,
      builtinLockUniv,
      builtinFromNat, builtinFromNeg, builtinFromString,
      builtinQName, builtinAgdaSort, builtinAgdaSortSet, builtinAgdaSortLit,
      builtinAgdaSortProp, builtinAgdaSortPropLit, builtinAgdaSortInf,
      builtinAgdaSortUnsupported,
      builtinHiding, builtinHidden, builtinInstance, builtinVisible,
      builtinRelevance, builtinRelevant, builtinIrrelevant,
      builtinQuantity, builtinQuantity0, builtinQuantityω,
      builtinModality, builtinModalityConstructor,
      builtinAssoc, builtinAssocLeft, builtinAssocRight, builtinAssocNon,
      builtinPrecedence, builtinPrecRelated, builtinPrecUnrelated,
      builtinFixity, builtinFixityFixity,
      builtinArgInfo, builtinArgArgInfo,
      builtinArg, builtinArgArg,
      builtinAbs, builtinAbsAbs, builtinAgdaTerm,
      builtinAgdaTermVar, builtinAgdaTermLam, builtinAgdaTermExtLam,
      builtinAgdaTermDef, builtinAgdaTermCon, builtinAgdaTermPi,
      builtinAgdaTermSort, builtinAgdaTermLit, builtinAgdaTermUnsupported, builtinAgdaTermMeta,
      builtinAgdaErrorPart, builtinAgdaErrorPartString, builtinAgdaErrorPartTerm, builtinAgdaErrorPartName,
      builtinAgdaLiteral, builtinAgdaLitNat, builtinAgdaLitWord64, builtinAgdaLitFloat,
      builtinAgdaLitChar, builtinAgdaLitString, builtinAgdaLitQName, builtinAgdaLitMeta,
      builtinAgdaClause, builtinAgdaClauseClause, builtinAgdaClauseAbsurd, builtinAgdaPattern,
      builtinAgdaPatVar, builtinAgdaPatCon, builtinAgdaPatDot, builtinAgdaPatLit,
      builtinAgdaPatProj, builtinAgdaPatAbsurd,
      builtinAgdaDefinitionFunDef,
      builtinAgdaDefinitionDataDef, builtinAgdaDefinitionRecordDef,
      builtinAgdaDefinitionDataConstructor, builtinAgdaDefinitionPostulate,
      builtinAgdaDefinitionPrimitive, builtinAgdaDefinition,
      builtinAgdaMeta,
      builtinAgdaTCM, builtinAgdaTCMReturn, builtinAgdaTCMBind, builtinAgdaTCMUnify,
      builtinAgdaTCMTypeError, builtinAgdaTCMInferType,
      builtinAgdaTCMCheckType, builtinAgdaTCMNormalise, builtinAgdaTCMReduce,
      builtinAgdaTCMCatchError,
      builtinAgdaTCMGetContext, builtinAgdaTCMExtendContext, builtinAgdaTCMInContext,
      builtinAgdaTCMFreshName, builtinAgdaTCMDeclareDef, builtinAgdaTCMDeclarePostulate, builtinAgdaTCMDefineFun,
      builtinAgdaTCMGetType, builtinAgdaTCMGetDefinition,
      builtinAgdaTCMQuoteTerm, builtinAgdaTCMUnquoteTerm, builtinAgdaTCMQuoteOmegaTerm,
      builtinAgdaTCMBlockOnMeta, builtinAgdaTCMCommit, builtinAgdaTCMIsMacro,
      builtinAgdaTCMWithNormalisation, builtinAgdaTCMWithReconsParams, builtinAgdaTCMDebugPrint,
      builtinAgdaTCMOnlyReduceDefs, builtinAgdaTCMDontReduceDefs,
      builtinAgdaTCMNoConstraints,
      builtinAgdaTCMRunSpeculative,
      builtinAgdaTCMExec
      :: String

    builtinNat :: String
    builtinNat                               = String
    "NATURAL"
    builtinSuc :: String
    builtinSuc                               = String
    "SUC"
    builtinZero :: String
    builtinZero                              = String
    "ZERO"
    builtinNatPlus :: String
    builtinNatPlus                           = String
    "NATPLUS"
    builtinNatMinus :: String
    builtinNatMinus                          = String
    "NATMINUS"
    builtinNatTimes :: String
    builtinNatTimes                          = String
    "NATTIMES"
    builtinNatDivSucAux :: String
    builtinNatDivSucAux                      = String
    "NATDIVSUCAUX"
    builtinNatModSucAux :: String
    builtinNatModSucAux                      = String
    "NATMODSUCAUX"
    builtinNatEquals :: String
    builtinNatEquals                         = String
    "NATEQUALS"
    builtinNatLess :: String
    builtinNatLess                           = String
    "NATLESS"
    builtinWord64 :: String
    builtinWord64                            = String
    "WORD64"
    builtinInteger :: String
    builtinInteger                           = String
    "INTEGER"
    builtinIntegerPos :: String
    builtinIntegerPos                        = String
    "INTEGERPOS"
    builtinIntegerNegSuc :: String
    builtinIntegerNegSuc                     = String
    "INTEGERNEGSUC"
    builtinFloat :: String
    builtinFloat                             = String
    "FLOAT"
    builtinChar :: String
    builtinChar                              = String
    "CHAR"
    builtinString :: String
    builtinString                            = String
    "STRING"
    builtinUnit :: String
    builtinUnit                              = String
    "UNIT"
    builtinUnitUnit :: String
    builtinUnitUnit                          = String
    "UNITUNIT"
    builtinSigma :: String
    builtinSigma                             = String
    "SIGMA"
    builtinBool :: String
    builtinBool                              = String
    "BOOL"
    builtinTrue :: String
    builtinTrue                              = String
    "TRUE"
    builtinFalse :: String
    builtinFalse                             = String
    "FALSE"
    builtinList :: String
    builtinList                              = String
    "LIST"
    builtinNil :: String
    builtinNil                               = String
    "NIL"
    builtinCons :: String
    builtinCons                              = String
    "CONS"
    builtinMaybe :: String
    builtinMaybe                             = String
    "MAYBE"
    builtinNothing :: String
    builtinNothing                           = String
    "NOTHING"
    builtinJust :: String
    builtinJust                              = String
    "JUST"
    builtinIO :: String
    builtinIO                                = String
    "IO"
    builtinId :: String
    builtinId                                = String
    "ID"
    builtinConId :: String
    builtinConId                             = String
    "CONID"
    builtinIdElim :: String
    builtinIdElim                            = String
    "primIdElim"
    builtinPath :: String
    builtinPath                              = String
    "PATH"
    builtinPathP :: String
    builtinPathP                             = String
    "PATHP"
    builtinInterval :: String
    builtinInterval                          = String
    "INTERVAL"
    builtinIMin :: String
    builtinIMin                              = String
    "primIMin"
    builtinIMax :: String
    builtinIMax                              = String
    "primIMax"
    builtinINeg :: String
    builtinINeg                              = String
    "primINeg"
    builtinIZero :: String
    builtinIZero                             = String
    "IZERO"
    builtinIOne :: String
    builtinIOne                              = String
    "IONE"
    builtinPartial :: String
    builtinPartial                           = String
    "PARTIAL"
    builtinPartialP :: String
    builtinPartialP                          = String
    "PARTIALP"
    builtinIsOne :: String
    builtinIsOne                             = String
    "ISONE"
    builtinItIsOne :: String
    builtinItIsOne                           = String
    "ITISONE"
    builtinEquiv :: String
    builtinEquiv                             = String
    "EQUIV"
    builtinEquivFun :: String
    builtinEquivFun                          = String
    "EQUIVFUN"
    builtinEquivProof :: String
    builtinEquivProof                        = String
    "EQUIVPROOF"
    builtinTranspProof :: String
    builtinTranspProof                       = String
    "TRANSPPROOF"
    builtinGlue :: String
    builtinGlue                              = String
    "primGlue"
    builtin_glue :: String
    builtin_glue                             = String
    "prim^glue"
    builtin_unglue :: String
    builtin_unglue                           = String
    "prim^unglue"
    builtin_glueU :: String
    builtin_glueU                            = String
    "prim^glueU"
    builtin_unglueU :: String
    builtin_unglueU                          = String
    "prim^unglueU"
    builtinFaceForall :: String
    builtinFaceForall                        = String
    "primFaceForall"
    builtinIsOne1 :: String
    builtinIsOne1                            = String
    "ISONE1"
    builtinIsOne2 :: String
    builtinIsOne2                            = String
    "ISONE2"
    builtinIsOneEmpty :: String
    builtinIsOneEmpty                        = String
    "ISONEEMPTY"
    builtinComp :: String
    builtinComp                              = String
    "primComp"
    builtinPOr :: String
    builtinPOr                               = String
    "primPOr"
    builtinTrans :: String
    builtinTrans                             = String
    "primTransp"
    builtinHComp :: String
    builtinHComp                             = String
    "primHComp"
    builtinSub :: String
    builtinSub                               = String
    "SUB"
    builtinSubIn :: String
    builtinSubIn                             = String
    "SUBIN"
    builtinSubOut :: String
    builtinSubOut                            = String
    "primSubOut"
    builtinSizeUniv :: String
    builtinSizeUniv                          = String
    "SIZEUNIV"
    builtinSize :: String
    builtinSize                              = String
    "SIZE"
    builtinSizeLt :: String
    builtinSizeLt                            = String
    "SIZELT"
    builtinSizeSuc :: String
    builtinSizeSuc                           = String
    "SIZESUC"
    builtinSizeInf :: String
    builtinSizeInf                           = String
    "SIZEINF"
    builtinSizeMax :: String
    builtinSizeMax                           = String
    "SIZEMAX"
    builtinInf :: String
    builtinInf                               = String
    "INFINITY"
    builtinSharp :: String
    builtinSharp                             = String
    "SHARP"
    builtinFlat :: String
    builtinFlat                              = String
    "FLAT"
    builtinEquality :: String
    builtinEquality                          = String
    "EQUALITY"
    builtinRefl :: String
    builtinRefl                              = String
    "REFL"
    builtinRewrite :: String
    builtinRewrite                           = String
    "REWRITE"
    builtinLevelMax :: String
    builtinLevelMax                          = String
    "LEVELMAX"
    builtinLevel :: String
    builtinLevel                             = String
    "LEVEL"
    builtinLevelZero :: String
    builtinLevelZero                         = String
    "LEVELZERO"
    builtinLevelSuc :: String
    builtinLevelSuc                          = String
    "LEVELSUC"
    builtinSet :: String
    builtinSet                               = String
    "TYPE"
    builtinProp :: String
    builtinProp                              = String
    "PROP"
    builtinSetOmega :: String
    builtinSetOmega                          = String
    "SETOMEGA"
    builtinLockUniv :: String
    builtinLockUniv                          = String
    "primLockUniv"
    builtinSSetOmega :: String
    builtinSSetOmega                         = String
    "STRICTSETOMEGA"
    builtinStrictSet :: String
    builtinStrictSet                         = String
    "STRICTSET"
    builtinFromNat :: String
    builtinFromNat                           = String
    "FROMNAT"
    builtinFromNeg :: String
    builtinFromNeg                           = String
    "FROMNEG"
    builtinFromString :: String
    builtinFromString                        = String
    "FROMSTRING"
    builtinQName :: String
    builtinQName                             = String
    "QNAME"
    builtinAgdaSort :: String
    builtinAgdaSort                          = String
    "AGDASORT"
    builtinAgdaSortSet :: String
    builtinAgdaSortSet                       = String
    "AGDASORTSET"
    builtinAgdaSortLit :: String
    builtinAgdaSortLit                       = String
    "AGDASORTLIT"
    builtinAgdaSortProp :: String
    builtinAgdaSortProp                      = String
    "AGDASORTPROP"
    builtinAgdaSortPropLit :: String
    builtinAgdaSortPropLit                   = String
    "AGDASORTPROPLIT"
    builtinAgdaSortInf :: String
    builtinAgdaSortInf                       = String
    "AGDASORTINF"
    builtinAgdaSortUnsupported :: String
    builtinAgdaSortUnsupported               = String
    "AGDASORTUNSUPPORTED"
    builtinHiding :: String
    builtinHiding                            = String
    "HIDING"
    builtinHidden :: String
    builtinHidden                            = String
    "HIDDEN"
    builtinInstance :: String
    builtinInstance                          = String
    "INSTANCE"
    builtinVisible :: String
    builtinVisible                           = String
    "VISIBLE"
    builtinRelevance :: String
    builtinRelevance                         = String
    "RELEVANCE"
    builtinRelevant :: String
    builtinRelevant                          = String
    "RELEVANT"
    builtinIrrelevant :: String
    builtinIrrelevant                        = String
    "IRRELEVANT"
    builtinQuantity :: String
    builtinQuantity                          = String
    "QUANTITY"
    builtinQuantity0 :: String
    builtinQuantity0                         = String
    "QUANTITY-0"
    builtinQuantityω :: String
    builtinQuantityω                         = String
    "QUANTITY-ω"
    builtinModality :: String
    builtinModality                          = String
    "MODALITY"
    builtinModalityConstructor :: String
    builtinModalityConstructor               = String
    "MODALITY-CONSTRUCTOR"
    builtinAssoc :: String
    builtinAssoc                             = String
    "ASSOC"
    builtinAssocLeft :: String
    builtinAssocLeft                         = String
    "ASSOCLEFT"
    builtinAssocRight :: String
    builtinAssocRight                        = String
    "ASSOCRIGHT"
    builtinAssocNon :: String
    builtinAssocNon                          = String
    "ASSOCNON"
    builtinPrecedence :: String
    builtinPrecedence                        = String
    "PRECEDENCE"
    builtinPrecRelated :: String
    builtinPrecRelated                       = String
    "PRECRELATED"
    builtinPrecUnrelated :: String
    builtinPrecUnrelated                     = String
    "PRECUNRELATED"
    builtinFixity :: String
    builtinFixity                            = String
    "FIXITY"
    builtinFixityFixity :: String
    builtinFixityFixity                      = String
    "FIXITYFIXITY"
    builtinArg :: String
    builtinArg                               = String
    "ARG"
    builtinArgInfo :: String
    builtinArgInfo                           = String
    "ARGINFO"
    builtinArgArgInfo :: String
    builtinArgArgInfo                        = String
    "ARGARGINFO"
    builtinArgArg :: String
    builtinArgArg                            = String
    "ARGARG"
    builtinAbs :: String
    builtinAbs                               = String
    "ABS"
    builtinAbsAbs :: String
    builtinAbsAbs                            = String
    "ABSABS"
    builtinAgdaTerm :: String
    builtinAgdaTerm                          = String
    "AGDATERM"
    builtinAgdaTermVar :: String
    builtinAgdaTermVar                       = String
    "AGDATERMVAR"
    builtinAgdaTermLam :: String
    builtinAgdaTermLam                       = String
    "AGDATERMLAM"
    builtinAgdaTermExtLam :: String
    builtinAgdaTermExtLam                    = String
    "AGDATERMEXTLAM"
    builtinAgdaTermDef :: String
    builtinAgdaTermDef                       = String
    "AGDATERMDEF"
    builtinAgdaTermCon :: String
    builtinAgdaTermCon                       = String
    "AGDATERMCON"
    builtinAgdaTermPi :: String
    builtinAgdaTermPi                        = String
    "AGDATERMPI"
    builtinAgdaTermSort :: String
    builtinAgdaTermSort                      = String
    "AGDATERMSORT"
    builtinAgdaTermLit :: String
    builtinAgdaTermLit                       = String
    "AGDATERMLIT"
    builtinAgdaTermUnsupported :: String
    builtinAgdaTermUnsupported               = String
    "AGDATERMUNSUPPORTED"
    builtinAgdaTermMeta :: String
    builtinAgdaTermMeta                      = String
    "AGDATERMMETA"
    builtinAgdaErrorPart :: String
    builtinAgdaErrorPart                     = String
    "AGDAERRORPART"
    builtinAgdaErrorPartString :: String
    builtinAgdaErrorPartString               = String
    "AGDAERRORPARTSTRING"
    builtinAgdaErrorPartTerm :: String
    builtinAgdaErrorPartTerm                 = String
    "AGDAERRORPARTTERM"
    builtinAgdaErrorPartName :: String
    builtinAgdaErrorPartName                 = String
    "AGDAERRORPARTNAME"
    builtinAgdaLiteral :: String
    builtinAgdaLiteral                       = String
    "AGDALITERAL"
    builtinAgdaLitNat :: String
    builtinAgdaLitNat                        = String
    "AGDALITNAT"
    builtinAgdaLitWord64 :: String
    builtinAgdaLitWord64                     = String
    "AGDALITWORD64"
    builtinAgdaLitFloat :: String
    builtinAgdaLitFloat                      = String
    "AGDALITFLOAT"
    builtinAgdaLitChar :: String
    builtinAgdaLitChar                       = String
    "AGDALITCHAR"
    builtinAgdaLitString :: String
    builtinAgdaLitString                     = String
    "AGDALITSTRING"
    builtinAgdaLitQName :: String
    builtinAgdaLitQName                      = String
    "AGDALITQNAME"
    builtinAgdaLitMeta :: String
    builtinAgdaLitMeta                       = String
    "AGDALITMETA"
    builtinAgdaClause :: String
    builtinAgdaClause                        = String
    "AGDACLAUSE"
    builtinAgdaClauseClause :: String
    builtinAgdaClauseClause                  = String
    "AGDACLAUSECLAUSE"
    builtinAgdaClauseAbsurd :: String
    builtinAgdaClauseAbsurd                  = String
    "AGDACLAUSEABSURD"
    builtinAgdaPattern :: String
    builtinAgdaPattern                       = String
    "AGDAPATTERN"
    builtinAgdaPatVar :: String
    builtinAgdaPatVar                        = String
    "AGDAPATVAR"
    builtinAgdaPatCon :: String
    builtinAgdaPatCon                        = String
    "AGDAPATCON"
    builtinAgdaPatDot :: String
    builtinAgdaPatDot                        = String
    "AGDAPATDOT"
    builtinAgdaPatLit :: String
    builtinAgdaPatLit                        = String
    "AGDAPATLIT"
    builtinAgdaPatProj :: String
    builtinAgdaPatProj                       = String
    "AGDAPATPROJ"
    builtinAgdaPatAbsurd :: String
    builtinAgdaPatAbsurd                     = String
    "AGDAPATABSURD"
    builtinAgdaDefinitionFunDef :: String
    builtinAgdaDefinitionFunDef              = String
    "AGDADEFINITIONFUNDEF"
    builtinAgdaDefinitionDataDef :: String
    builtinAgdaDefinitionDataDef             = String
    "AGDADEFINITIONDATADEF"
    builtinAgdaDefinitionRecordDef :: String
    builtinAgdaDefinitionRecordDef           = String
    "AGDADEFINITIONRECORDDEF"
    builtinAgdaDefinitionDataConstructor :: String
    builtinAgdaDefinitionDataConstructor     = String
    "AGDADEFINITIONDATACONSTRUCTOR"
    builtinAgdaDefinitionPostulate :: String
    builtinAgdaDefinitionPostulate           = String
    "AGDADEFINITIONPOSTULATE"
    builtinAgdaDefinitionPrimitive :: String
    builtinAgdaDefinitionPrimitive           = String
    "AGDADEFINITIONPRIMITIVE"
    builtinAgdaDefinition :: String
    builtinAgdaDefinition                    = String
    "AGDADEFINITION"
    builtinAgdaMeta :: String
    builtinAgdaMeta                          = String
    "AGDAMETA"
    builtinAgdaTCM :: String
    builtinAgdaTCM                           = String
    "AGDATCM"
    builtinAgdaTCMReturn :: String
    builtinAgdaTCMReturn                     = String
    "AGDATCMRETURN"
    builtinAgdaTCMBind :: String
    builtinAgdaTCMBind                       = String
    "AGDATCMBIND"
    builtinAgdaTCMUnify :: String
    builtinAgdaTCMUnify                      = String
    "AGDATCMUNIFY"
    builtinAgdaTCMTypeError :: String
    builtinAgdaTCMTypeError                  = String
    "AGDATCMTYPEERROR"
    builtinAgdaTCMInferType :: String
    builtinAgdaTCMInferType                  = String
    "AGDATCMINFERTYPE"
    builtinAgdaTCMCheckType :: String
    builtinAgdaTCMCheckType                  = String
    "AGDATCMCHECKTYPE"
    builtinAgdaTCMNormalise :: String
    builtinAgdaTCMNormalise                  = String
    "AGDATCMNORMALISE"
    builtinAgdaTCMReduce :: String
    builtinAgdaTCMReduce                     = String
    "AGDATCMREDUCE"
    builtinAgdaTCMCatchError :: String
    builtinAgdaTCMCatchError                 = String
    "AGDATCMCATCHERROR"
    builtinAgdaTCMGetContext :: String
    builtinAgdaTCMGetContext                 = String
    "AGDATCMGETCONTEXT"
    builtinAgdaTCMExtendContext :: String
    builtinAgdaTCMExtendContext              = String
    "AGDATCMEXTENDCONTEXT"
    builtinAgdaTCMInContext :: String
    builtinAgdaTCMInContext                  = String
    "AGDATCMINCONTEXT"
    builtinAgdaTCMFreshName :: String
    builtinAgdaTCMFreshName                  = String
    "AGDATCMFRESHNAME"
    builtinAgdaTCMDeclareDef :: String
    builtinAgdaTCMDeclareDef                 = String
    "AGDATCMDECLAREDEF"
    builtinAgdaTCMDeclarePostulate :: String
    builtinAgdaTCMDeclarePostulate           = String
    "AGDATCMDECLAREPOSTULATE"
    builtinAgdaTCMDefineFun :: String
    builtinAgdaTCMDefineFun                  = String
    "AGDATCMDEFINEFUN"
    builtinAgdaTCMGetType :: String
    builtinAgdaTCMGetType                    = String
    "AGDATCMGETTYPE"
    builtinAgdaTCMGetDefinition :: String
    builtinAgdaTCMGetDefinition              = String
    "AGDATCMGETDEFINITION"
    builtinAgdaTCMBlockOnMeta :: String
    builtinAgdaTCMBlockOnMeta                = String
    "AGDATCMBLOCKONMETA"
    builtinAgdaTCMCommit :: String
    builtinAgdaTCMCommit                     = String
    "AGDATCMCOMMIT"
    builtinAgdaTCMQuoteTerm :: String
    builtinAgdaTCMQuoteTerm                  = String
    "AGDATCMQUOTETERM"
    builtinAgdaTCMUnquoteTerm :: String
    builtinAgdaTCMUnquoteTerm                = String
    "AGDATCMUNQUOTETERM"
    builtinAgdaTCMQuoteOmegaTerm :: String
    builtinAgdaTCMQuoteOmegaTerm             = String
    "AGDATCMQUOTEOMEGATERM"
    builtinAgdaTCMIsMacro :: String
    builtinAgdaTCMIsMacro                    = String
    "AGDATCMISMACRO"
    builtinAgdaTCMWithNormalisation :: String
    builtinAgdaTCMWithNormalisation          = String
    "AGDATCMWITHNORMALISATION"
    builtinAgdaTCMWithReconsParams :: String
    builtinAgdaTCMWithReconsParams           = String
    "AGDATCMWITHRECONSPARAMS"
    builtinAgdaTCMDebugPrint :: String
    builtinAgdaTCMDebugPrint                 = String
    "AGDATCMDEBUGPRINT"
    builtinAgdaTCMOnlyReduceDefs :: String
    builtinAgdaTCMOnlyReduceDefs             = String
    "AGDATCMONLYREDUCEDEFS"
    builtinAgdaTCMDontReduceDefs :: String
    builtinAgdaTCMDontReduceDefs             = String
    "AGDATCMDONTREDUCEDEFS"
    builtinAgdaTCMNoConstraints :: String
    builtinAgdaTCMNoConstraints              = String
    "AGDATCMNOCONSTRAINTS"
    builtinAgdaTCMRunSpeculative :: String
    builtinAgdaTCMRunSpeculative             = String
    "AGDATCMRUNSPECULATIVE"
    builtinAgdaTCMExec :: String
    builtinAgdaTCMExec                       = String
    "AGDATCMEXEC"

    -- | 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.

    isBuiltinNoDef :: String -> Bool
    isBuiltinNoDef :: String -> Bool
    isBuiltinNoDef = [String] -> String -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [String]
    builtinsNoDef

    builtinsNoDef :: [String]
    builtinsNoDef :: [String]
    builtinsNoDef =
      [String]
    sizeBuiltins [String] -> [String] -> [String]
    forall a. [a] -> [a] -> [a]
    ++
      [ String
    builtinConId
      , String
    builtinInterval
      , String
    builtinPartial
      , String
    builtinPartialP
      , String
    builtinIsOne
      , String
    builtinSub
      , String
    builtinIZero
      , String
    builtinIOne
      , String
    builtinSet
      , String
    builtinProp
      , String
    builtinSetOmega
      , String
    builtinStrictSet
      , String
    builtinSSetOmega
      ]

    sizeBuiltins :: [String]
    sizeBuiltins :: [String]
    sizeBuiltins =
      [ String
    builtinSizeUniv
      , String
    builtinSize
      , String
    builtinSizeLt
      , String
    builtinSizeSuc
      , String
    builtinSizeInf
      , String
    builtinSizeMax
      ]