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

    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,
      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, builtinPathToEquiv,
      builtinGlue, builtin_glue, builtin_unglue,
      builtinFaceForall,
      builtinId, builtinConId, builtinIdElim,
      builtinSizeUniv, builtinSize, builtinSizeLt,
      builtinSizeSuc, builtinSizeInf, builtinSizeMax,
      builtinInf, builtinSharp, builtinFlat,
      builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
      builtinLevel, builtinLevelZero, builtinLevelSuc,
      builtinSetOmega,
      builtinFromNat, builtinFromNeg, builtinFromString,
      builtinQName, builtinAgdaSort, builtinAgdaSortSet, builtinAgdaSortLit,
      builtinAgdaSortUnsupported,
      builtinHiding, builtinHidden, builtinInstance, builtinVisible,
      builtinRelevance, builtinRelevant, builtinIrrelevant, builtinArg,
      builtinAssoc, builtinAssocLeft, builtinAssocRight, builtinAssocNon,
      builtinPrecedence, builtinPrecRelated, builtinPrecUnrelated,
      builtinFixity, builtinFixityFixity,
      builtinArgInfo, builtinArgArgInfo, 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,
      builtinAgdaTCMBlockOnMeta, builtinAgdaTCMCommit, builtinAgdaTCMIsMacro,
      builtinAgdaTCMWithNormalisation, builtinAgdaTCMDebugPrint,
      builtinAgdaTCMNoConstraints,
      builtinAgdaTCMRunSpeculative
      :: String

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

    -- | 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]
    builtinsNoDef =
      sizeBuiltins ++
      [ builtinConId
      , builtinInterval
      , builtinPartial
      , builtinPartialP
      , builtinIsOne
      , builtinSub
      , builtinIZero
      , builtinIOne
      , builtinSetOmega
      ]

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