    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | This module defines the names of all builtin and primitives used in Agda.
    --
    -- See "Agda.TypeChecking.Monad.Builtin"
    module Agda.Syntax.Builtin where

    import GHC.Generics (Generic)

    import Control.DeepSeq (NFData)

    import qualified Data.Map as M
    import Data.Hashable

    import Agda.Syntax.Common.Pretty
    import Agda.Syntax.Position

    import Agda.Utils.List

    -- | Either a 'BuiltinId' or 'PrimitiveId', used for some lookups.
    data SomeBuiltin
      = BuiltinName !BuiltinId
      | PrimitiveName !PrimitiveId
      deriving (Int -> SomeBuiltin -> ShowS
    [SomeBuiltin] -> ShowS
    SomeBuiltin -> String
    (Int -> SomeBuiltin -> ShowS)
    -> (SomeBuiltin -> String)
    -> ([SomeBuiltin] -> ShowS)
    -> Show SomeBuiltin
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SomeBuiltin -> ShowS
    showsPrec :: Int -> SomeBuiltin -> ShowS
    $cshow :: SomeBuiltin -> String
    show :: SomeBuiltin -> String
    $cshowList :: [SomeBuiltin] -> ShowS
    showList :: [SomeBuiltin] -> ShowS
    Show, SomeBuiltin -> SomeBuiltin -> Bool
    (SomeBuiltin -> SomeBuiltin -> Bool)
    -> (SomeBuiltin -> SomeBuiltin -> Bool) -> Eq SomeBuiltin
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: SomeBuiltin -> SomeBuiltin -> Bool
    == :: SomeBuiltin -> SomeBuiltin -> Bool
    $c/= :: SomeBuiltin -> SomeBuiltin -> Bool
    /= :: SomeBuiltin -> SomeBuiltin -> Bool
    Eq, Eq SomeBuiltin
    Eq SomeBuiltin =>
    (SomeBuiltin -> SomeBuiltin -> Ordering)
    -> (SomeBuiltin -> SomeBuiltin -> Bool)
    -> (SomeBuiltin -> SomeBuiltin -> Bool)
    -> (SomeBuiltin -> SomeBuiltin -> Bool)
    -> (SomeBuiltin -> SomeBuiltin -> Bool)
    -> (SomeBuiltin -> SomeBuiltin -> SomeBuiltin)
    -> (SomeBuiltin -> SomeBuiltin -> SomeBuiltin)
    -> Ord SomeBuiltin
    SomeBuiltin -> SomeBuiltin -> Bool
    SomeBuiltin -> SomeBuiltin -> Ordering
    SomeBuiltin -> SomeBuiltin -> SomeBuiltin
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: SomeBuiltin -> SomeBuiltin -> Ordering
    compare :: SomeBuiltin -> SomeBuiltin -> Ordering
    $c< :: SomeBuiltin -> SomeBuiltin -> Bool
    < :: SomeBuiltin -> SomeBuiltin -> Bool
    $c<= :: SomeBuiltin -> SomeBuiltin -> Bool
    <= :: SomeBuiltin -> SomeBuiltin -> Bool
    $c> :: SomeBuiltin -> SomeBuiltin -> Bool
    > :: SomeBuiltin -> SomeBuiltin -> Bool
    $c>= :: SomeBuiltin -> SomeBuiltin -> Bool
    >= :: SomeBuiltin -> SomeBuiltin -> Bool
    $cmax :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
    max :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
    $cmin :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
    min :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin
    Ord, (forall x. SomeBuiltin -> Rep SomeBuiltin x)
    -> (forall x. Rep SomeBuiltin x -> SomeBuiltin)
    -> Generic SomeBuiltin
    forall x. Rep SomeBuiltin x -> SomeBuiltin
    forall x. SomeBuiltin -> Rep SomeBuiltin x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SomeBuiltin -> Rep SomeBuiltin x
    from :: forall x. SomeBuiltin -> Rep SomeBuiltin x
    $cto :: forall x. Rep SomeBuiltin x -> SomeBuiltin
    to :: forall x. Rep SomeBuiltin x -> SomeBuiltin
    Generic)

    instance Hashable SomeBuiltin
    instance NFData SomeBuiltin

    -- | The class of types which can be converted to 'SomeBuiltin'.
    class IsBuiltin a where
      -- | Convert this value to a builtin.
      someBuiltin :: a -> SomeBuiltin

      -- | Get the identifier for this builtin, generally used for error messages.
      getBuiltinId :: a -> String

    instance IsBuiltin SomeBuiltin where
      someBuiltin :: SomeBuiltin -> SomeBuiltin
    someBuiltin = SomeBuiltin -> SomeBuiltin
    forall a. a -> a
    id

      getBuiltinId :: SomeBuiltin -> String
    getBuiltinId (BuiltinName BuiltinId
    x) = BuiltinId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId BuiltinId
    x
      getBuiltinId (PrimitiveName PrimitiveId
    x) = PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    x

    -- * Builtins

    -- | A builtin name, defined by the @BUILTIN@ pragma.
    data BuiltinId
      = BuiltinNat
      | BuiltinSuc
      | BuiltinZero
      | BuiltinNatPlus
      | BuiltinNatMinus
      | BuiltinNatTimes
      | BuiltinNatDivSucAux
      | BuiltinNatModSucAux
      | BuiltinNatEquals
      | BuiltinNatLess
      | BuiltinWord64
      | BuiltinInteger
      | BuiltinIntegerPos
      | BuiltinIntegerNegSuc
      | BuiltinFloat
      | BuiltinChar
      | BuiltinString
      | BuiltinUnit
      | BuiltinUnitUnit
      | BuiltinSigma
      | BuiltinSigmaCon
      | BuiltinBool
      | BuiltinTrue
      | BuiltinFalse
      | BuiltinList
      | BuiltinNil
      | BuiltinCons
      | BuiltinMaybe
      | BuiltinNothing
      | BuiltinJust
      | BuiltinIO
      | BuiltinPath
      | BuiltinPathP
      | BuiltinIntervalUniv
      | BuiltinInterval
      | BuiltinIZero
      | BuiltinIOne
      | BuiltinPartial
      | BuiltinPartialP
      | BuiltinIsOne
      | BuiltinItIsOne
      | BuiltinEquiv
      | BuiltinEquivFun
      | BuiltinEquivProof
      | BuiltinTranspProof
      | BuiltinIsOne1
      | BuiltinIsOne2
      | BuiltinIsOneEmpty
      | BuiltinSub
      | BuiltinSubIn
      | BuiltinSizeUniv
      | BuiltinSize
      | BuiltinSizeLt
      | BuiltinSizeSuc
      | BuiltinSizeInf
      | BuiltinSizeMax
      | BuiltinInf
      | BuiltinSharp
      | BuiltinFlat
      | BuiltinEquality
      | BuiltinRefl
      | BuiltinRewrite
      | BuiltinLevelMax
      | BuiltinLevel
      | BuiltinLevelZero
      | BuiltinLevelSuc
      | BuiltinProp
      | BuiltinSet
      | BuiltinStrictSet
      | BuiltinPropOmega
      | BuiltinSetOmega
      | BuiltinSSetOmega
      | BuiltinLevelUniv
      | 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
      | BuiltinArg
      | BuiltinArgInfo
      | BuiltinArgArgInfo
      | BuiltinArgArg
      | BuiltinAbs
      | BuiltinAbsAbs
      | BuiltinAgdaTerm
      | BuiltinAgdaTermVar
      | BuiltinAgdaTermLam
      | BuiltinAgdaTermExtLam
      | BuiltinAgdaTermDef
      | BuiltinAgdaTermCon
      | BuiltinAgdaTermPi
      | BuiltinAgdaTermSort
      | BuiltinAgdaTermLit
      | BuiltinAgdaTermUnsupported
      | BuiltinAgdaTermMeta
      | BuiltinAgdaErrorPart
      | BuiltinAgdaErrorPartString
      | BuiltinAgdaErrorPartTerm
      | BuiltinAgdaErrorPartPatt
      | 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
      | BuiltinAgdaTCMDeclareData
      | BuiltinAgdaTCMDefineData
      | BuiltinAgdaTCMDefineFun
      | BuiltinAgdaTCMGetType
      | BuiltinAgdaTCMGetDefinition
      | BuiltinAgdaTCMBlock
      | BuiltinAgdaTCMCommit
      | BuiltinAgdaTCMQuoteTerm
      | BuiltinAgdaTCMUnquoteTerm
      | BuiltinAgdaTCMQuoteOmegaTerm
      | BuiltinAgdaTCMIsMacro
      | BuiltinAgdaTCMWithNormalisation
      | BuiltinAgdaTCMWithReconstructed
      | BuiltinAgdaTCMWithExpandLast
      | BuiltinAgdaTCMWithReduceDefs
      | BuiltinAgdaTCMAskNormalisation
      | BuiltinAgdaTCMAskReconstructed
      | BuiltinAgdaTCMAskExpandLast
      | BuiltinAgdaTCMAskReduceDefs
      | BuiltinAgdaTCMFormatErrorParts
      | BuiltinAgdaTCMDebugPrint
      | BuiltinAgdaTCMNoConstraints
      | BuiltinAgdaTCMWorkOnTypes
      | BuiltinAgdaTCMRunSpeculative
      | BuiltinAgdaTCMExec
      | BuiltinAgdaTCMCheckFromString
      | BuiltinAgdaTCMGetInstances
      | BuiltinAgdaTCMSolveInstances
      | BuiltinAgdaTCMPragmaForeign
      | BuiltinAgdaTCMPragmaCompile
      | BuiltinAgdaBlocker
      | BuiltinAgdaBlockerAny
      | BuiltinAgdaBlockerAll
      | BuiltinAgdaBlockerMeta
      deriving (Int -> BuiltinId -> ShowS
    [BuiltinId] -> ShowS
    BuiltinId -> String
    (Int -> BuiltinId -> ShowS)
    -> (BuiltinId -> String)
    -> ([BuiltinId] -> ShowS)
    -> Show BuiltinId
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> BuiltinId -> ShowS
    showsPrec :: Int -> BuiltinId -> ShowS
    $cshow :: BuiltinId -> String
    show :: BuiltinId -> String
    $cshowList :: [BuiltinId] -> ShowS
    showList :: [BuiltinId] -> ShowS
    Show, BuiltinId -> BuiltinId -> Bool
    (BuiltinId -> BuiltinId -> Bool)
    -> (BuiltinId -> BuiltinId -> Bool) -> Eq BuiltinId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: BuiltinId -> BuiltinId -> Bool
    == :: BuiltinId -> BuiltinId -> Bool
    $c/= :: BuiltinId -> BuiltinId -> Bool
    /= :: BuiltinId -> BuiltinId -> Bool
    Eq, Eq BuiltinId
    Eq BuiltinId =>
    (BuiltinId -> BuiltinId -> Ordering)
    -> (BuiltinId -> BuiltinId -> Bool)
    -> (BuiltinId -> BuiltinId -> Bool)
    -> (BuiltinId -> BuiltinId -> Bool)
    -> (BuiltinId -> BuiltinId -> Bool)
    -> (BuiltinId -> BuiltinId -> BuiltinId)
    -> (BuiltinId -> BuiltinId -> BuiltinId)
    -> Ord BuiltinId
    BuiltinId -> BuiltinId -> Bool
    BuiltinId -> BuiltinId -> Ordering
    BuiltinId -> BuiltinId -> BuiltinId
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: BuiltinId -> BuiltinId -> Ordering
    compare :: BuiltinId -> BuiltinId -> Ordering
    $c< :: BuiltinId -> BuiltinId -> Bool
    < :: BuiltinId -> BuiltinId -> Bool
    $c<= :: BuiltinId -> BuiltinId -> Bool
    <= :: BuiltinId -> BuiltinId -> Bool
    $c> :: BuiltinId -> BuiltinId -> Bool
    > :: BuiltinId -> BuiltinId -> Bool
    $c>= :: BuiltinId -> BuiltinId -> Bool
    >= :: BuiltinId -> BuiltinId -> Bool
    $cmax :: BuiltinId -> BuiltinId -> BuiltinId
    max :: BuiltinId -> BuiltinId -> BuiltinId
    $cmin :: BuiltinId -> BuiltinId -> BuiltinId
    min :: BuiltinId -> BuiltinId -> BuiltinId
    Ord, BuiltinId
    BuiltinId -> BuiltinId -> Bounded BuiltinId
    forall a. a -> a -> Bounded a
    $cminBound :: BuiltinId
    minBound :: BuiltinId
    $cmaxBound :: BuiltinId
    maxBound :: BuiltinId
    Bounded, Int -> BuiltinId
    BuiltinId -> Int
    BuiltinId -> [BuiltinId]
    BuiltinId -> BuiltinId
    BuiltinId -> BuiltinId -> [BuiltinId]
    BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
    (BuiltinId -> BuiltinId)
    -> (BuiltinId -> BuiltinId)
    -> (Int -> BuiltinId)
    -> (BuiltinId -> Int)
    -> (BuiltinId -> [BuiltinId])
    -> (BuiltinId -> BuiltinId -> [BuiltinId])
    -> (BuiltinId -> BuiltinId -> [BuiltinId])
    -> (BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId])
    -> Enum BuiltinId
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: BuiltinId -> BuiltinId
    succ :: BuiltinId -> BuiltinId
    $cpred :: BuiltinId -> BuiltinId
    pred :: BuiltinId -> BuiltinId
    $ctoEnum :: Int -> BuiltinId
    toEnum :: Int -> BuiltinId
    $cfromEnum :: BuiltinId -> Int
    fromEnum :: BuiltinId -> Int
    $cenumFrom :: BuiltinId -> [BuiltinId]
    enumFrom :: BuiltinId -> [BuiltinId]
    $cenumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId]
    enumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId]
    $cenumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId]
    enumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId]
    $cenumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
    enumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]
    Enum, (forall x. BuiltinId -> Rep BuiltinId x)
    -> (forall x. Rep BuiltinId x -> BuiltinId) -> Generic BuiltinId
    forall x. Rep BuiltinId x -> BuiltinId
    forall x. BuiltinId -> Rep BuiltinId x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. BuiltinId -> Rep BuiltinId x
    from :: forall x. BuiltinId -> Rep BuiltinId x
    $cto :: forall x. Rep BuiltinId x -> BuiltinId
    to :: forall x. Rep BuiltinId x -> BuiltinId
    Generic)

    instance NFData BuiltinId

    instance Hashable BuiltinId where
      Int
    s hashWithSalt :: Int -> BuiltinId -> Int
    `hashWithSalt` BuiltinId
    b = Int
    s Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` BuiltinId -> Int
    forall a. Enum a => a -> Int
    fromEnum BuiltinId
    b

    instance KillRange BuiltinId where
      killRange :: BuiltinId -> BuiltinId
    killRange = BuiltinId -> BuiltinId
    forall a. a -> a
    id

    instance Pretty BuiltinId where
      pretty :: BuiltinId -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> (BuiltinId -> String) -> BuiltinId -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . BuiltinId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId

    instance IsBuiltin BuiltinId where
      someBuiltin :: BuiltinId -> SomeBuiltin
    someBuiltin = BuiltinId -> SomeBuiltin
    BuiltinName

      getBuiltinId :: BuiltinId -> String
    getBuiltinId = \case
        BuiltinId
    BuiltinNat                               -> String
    "NATURAL"
        BuiltinId
    BuiltinSuc                               -> String
    "SUC"
        BuiltinId
    BuiltinZero                              -> String
    "ZERO"
        BuiltinId
    BuiltinNatPlus                           -> String
    "NATPLUS"
        BuiltinId
    BuiltinNatMinus                          -> String
    "NATMINUS"
        BuiltinId
    BuiltinNatTimes                          -> String
    "NATTIMES"
        BuiltinId
    BuiltinNatDivSucAux                      -> String
    "NATDIVSUCAUX"
        BuiltinId
    BuiltinNatModSucAux                      -> String
    "NATMODSUCAUX"
        BuiltinId
    BuiltinNatEquals                         -> String
    "NATEQUALS"
        BuiltinId
    BuiltinNatLess                           -> String
    "NATLESS"
        BuiltinId
    BuiltinWord64                            -> String
    "WORD64"
        BuiltinId
    BuiltinInteger                           -> String
    "INTEGER"
        BuiltinId
    BuiltinIntegerPos                        -> String
    "INTEGERPOS"
        BuiltinId
    BuiltinIntegerNegSuc                     -> String
    "INTEGERNEGSUC"
        BuiltinId
    BuiltinFloat                             -> String
    "FLOAT"
        BuiltinId
    BuiltinChar                              -> String
    "CHAR"
        BuiltinId
    BuiltinString                            -> String
    "STRING"
        BuiltinId
    BuiltinUnit                              -> String
    "UNIT"
        BuiltinId
    BuiltinUnitUnit                          -> String
    "UNITUNIT"
        BuiltinId
    BuiltinSigma                             -> String
    "SIGMA"
        BuiltinId
    BuiltinSigmaCon                          -> String
    "SIGMACON"
        BuiltinId
    BuiltinBool                              -> String
    "BOOL"
        BuiltinId
    BuiltinTrue                              -> String
    "TRUE"
        BuiltinId
    BuiltinFalse                             -> String
    "FALSE"
        BuiltinId
    BuiltinList                              -> String
    "LIST"
        BuiltinId
    BuiltinNil                               -> String
    "NIL"
        BuiltinId
    BuiltinCons                              -> String
    "CONS"
        BuiltinId
    BuiltinMaybe                             -> String
    "MAYBE"
        BuiltinId
    BuiltinNothing                           -> String
    "NOTHING"
        BuiltinId
    BuiltinJust                              -> String
    "JUST"
        BuiltinId
    BuiltinIO                                -> String
    "IO"
        BuiltinId
    BuiltinPath                              -> String
    "PATH"
        BuiltinId
    BuiltinPathP                             -> String
    "PATHP"
        BuiltinId
    BuiltinIntervalUniv                      -> String
    "CUBEINTERVALUNIV"
        BuiltinId
    BuiltinInterval                          -> String
    "INTERVAL"
        BuiltinId
    BuiltinIZero                             -> String
    "IZERO"
        BuiltinId
    BuiltinIOne                              -> String
    "IONE"
        BuiltinId
    BuiltinPartial                           -> String
    "PARTIAL"
        BuiltinId
    BuiltinPartialP                          -> String
    "PARTIALP"
        BuiltinId
    BuiltinIsOne                             -> String
    "ISONE"
        BuiltinId
    BuiltinItIsOne                           -> String
    "ITISONE"
        BuiltinId
    BuiltinEquiv                             -> String
    "EQUIV"
        BuiltinId
    BuiltinEquivFun                          -> String
    "EQUIVFUN"
        BuiltinId
    BuiltinEquivProof                        -> String
    "EQUIVPROOF"
        BuiltinId
    BuiltinTranspProof                       -> String
    "TRANSPPROOF"
        BuiltinId
    BuiltinIsOne1                            -> String
    "ISONE1"
        BuiltinId
    BuiltinIsOne2                            -> String
    "ISONE2"
        BuiltinId
    BuiltinIsOneEmpty                        -> String
    "ISONEEMPTY"
        BuiltinId
    BuiltinSub                               -> String
    "SUB"
        BuiltinId
    BuiltinSubIn                             -> String
    "SUBIN"
        BuiltinId
    BuiltinSizeUniv                          -> String
    "SIZEUNIV"
        BuiltinId
    BuiltinSize                              -> String
    "SIZE"
        BuiltinId
    BuiltinSizeLt                            -> String
    "SIZELT"
        BuiltinId
    BuiltinSizeSuc                           -> String
    "SIZESUC"
        BuiltinId
    BuiltinSizeInf                           -> String
    "SIZEINF"
        BuiltinId
    BuiltinSizeMax                           -> String
    "SIZEMAX"
        BuiltinId
    BuiltinInf                               -> String
    "INFINITY"
        BuiltinId
    BuiltinSharp                             -> String
    "SHARP"
        BuiltinId
    BuiltinFlat                              -> String
    "FLAT"
        BuiltinId
    BuiltinEquality                          -> String
    "EQUALITY"
        BuiltinId
    BuiltinRefl                              -> String
    "REFL"
        BuiltinId
    BuiltinRewrite                           -> String
    "REWRITE"
        BuiltinId
    BuiltinLevelMax                          -> String
    "LEVELMAX"
        BuiltinId
    BuiltinLevel                             -> String
    "LEVEL"
        BuiltinId
    BuiltinLevelZero                         -> String
    "LEVELZERO"
        BuiltinId
    BuiltinLevelSuc                          -> String
    "LEVELSUC"
        BuiltinId
    BuiltinProp                              -> String
    "PROP"
        BuiltinId
    BuiltinSet                               -> String
    "TYPE"
        BuiltinId
    BuiltinStrictSet                         -> String
    "STRICTSET"
        BuiltinId
    BuiltinPropOmega                         -> String
    "PROPOMEGA"
        BuiltinId
    BuiltinSetOmega                          -> String
    "SETOMEGA"
        BuiltinId
    BuiltinSSetOmega                         -> String
    "STRICTSETOMEGA"
        BuiltinId
    BuiltinLevelUniv                         -> String
    "LEVELUNIV"
        BuiltinId
    BuiltinFromNat                           -> String
    "FROMNAT"
        BuiltinId
    BuiltinFromNeg                           -> String
    "FROMNEG"
        BuiltinId
    BuiltinFromString                        -> String
    "FROMSTRING"
        BuiltinId
    BuiltinQName                             -> String
    "QNAME"
        BuiltinId
    BuiltinAgdaSort                          -> String
    "AGDASORT"
        BuiltinId
    BuiltinAgdaSortSet                       -> String
    "AGDASORTSET"
        BuiltinId
    BuiltinAgdaSortLit                       -> String
    "AGDASORTLIT"
        BuiltinId
    BuiltinAgdaSortProp                      -> String
    "AGDASORTPROP"
        BuiltinId
    BuiltinAgdaSortPropLit                   -> String
    "AGDASORTPROPLIT"
        BuiltinId
    BuiltinAgdaSortInf                       -> String
    "AGDASORTINF"
        BuiltinId
    BuiltinAgdaSortUnsupported               -> String
    "AGDASORTUNSUPPORTED"
        BuiltinId
    BuiltinHiding                            -> String
    "HIDING"
        BuiltinId
    BuiltinHidden                            -> String
    "HIDDEN"
        BuiltinId
    BuiltinInstance                          -> String
    "INSTANCE"
        BuiltinId
    BuiltinVisible                           -> String
    "VISIBLE"
        BuiltinId
    BuiltinRelevance                         -> String
    "RELEVANCE"
        BuiltinId
    BuiltinRelevant                          -> String
    "RELEVANT"
        BuiltinId
    BuiltinIrrelevant                        -> String
    "IRRELEVANT"
        BuiltinId
    BuiltinQuantity                          -> String
    "QUANTITY"
        BuiltinId
    BuiltinQuantity0                         -> String
    "QUANTITY-0"
        BuiltinId
    BuiltinQuantityω                         -> String
    "QUANTITY-ω"
        BuiltinId
    BuiltinModality                          -> String
    "MODALITY"
        BuiltinId
    BuiltinModalityConstructor               -> String
    "MODALITY-CONSTRUCTOR"
        BuiltinId
    BuiltinAssoc                             -> String
    "ASSOC"
        BuiltinId
    BuiltinAssocLeft                         -> String
    "ASSOCLEFT"
        BuiltinId
    BuiltinAssocRight                        -> String
    "ASSOCRIGHT"
        BuiltinId
    BuiltinAssocNon                          -> String
    "ASSOCNON"
        BuiltinId
    BuiltinPrecedence                        -> String
    "PRECEDENCE"
        BuiltinId
    BuiltinPrecRelated                       -> String
    "PRECRELATED"
        BuiltinId
    BuiltinPrecUnrelated                     -> String
    "PRECUNRELATED"
        BuiltinId
    BuiltinFixity                            -> String
    "FIXITY"
        BuiltinId
    BuiltinFixityFixity                      -> String
    "FIXITYFIXITY"
        BuiltinId
    BuiltinArg                               -> String
    "ARG"
        BuiltinId
    BuiltinArgInfo                           -> String
    "ARGINFO"
        BuiltinId
    BuiltinArgArgInfo                        -> String
    "ARGARGINFO"
        BuiltinId
    BuiltinArgArg                            -> String
    "ARGARG"
        BuiltinId
    BuiltinAbs                               -> String
    "ABS"
        BuiltinId
    BuiltinAbsAbs                            -> String
    "ABSABS"
        BuiltinId
    BuiltinAgdaTerm                          -> String
    "AGDATERM"
        BuiltinId
    BuiltinAgdaTermVar                       -> String
    "AGDATERMVAR"
        BuiltinId
    BuiltinAgdaTermLam                       -> String
    "AGDATERMLAM"
        BuiltinId
    BuiltinAgdaTermExtLam                    -> String
    "AGDATERMEXTLAM"
        BuiltinId
    BuiltinAgdaTermDef                       -> String
    "AGDATERMDEF"
        BuiltinId
    BuiltinAgdaTermCon                       -> String
    "AGDATERMCON"
        BuiltinId
    BuiltinAgdaTermPi                        -> String
    "AGDATERMPI"
        BuiltinId
    BuiltinAgdaTermSort                      -> String
    "AGDATERMSORT"
        BuiltinId
    BuiltinAgdaTermLit                       -> String
    "AGDATERMLIT"
        BuiltinId
    BuiltinAgdaTermUnsupported               -> String
    "AGDATERMUNSUPPORTED"
        BuiltinId
    BuiltinAgdaTermMeta                      -> String
    "AGDATERMMETA"
        BuiltinId
    BuiltinAgdaErrorPart                     -> String
    "AGDAERRORPART"
        BuiltinId
    BuiltinAgdaErrorPartString               -> String
    "AGDAERRORPARTSTRING"
        BuiltinId
    BuiltinAgdaErrorPartTerm                 -> String
    "AGDAERRORPARTTERM"
        BuiltinId
    BuiltinAgdaErrorPartPatt                 -> String
    "AGDAERRORPARTPATT"
        BuiltinId
    BuiltinAgdaErrorPartName                 -> String
    "AGDAERRORPARTNAME"
        BuiltinId
    BuiltinAgdaLiteral                       -> String
    "AGDALITERAL"
        BuiltinId
    BuiltinAgdaLitNat                        -> String
    "AGDALITNAT"
        BuiltinId
    BuiltinAgdaLitWord64                     -> String
    "AGDALITWORD64"
        BuiltinId
    BuiltinAgdaLitFloat                      -> String
    "AGDALITFLOAT"
        BuiltinId
    BuiltinAgdaLitChar                       -> String
    "AGDALITCHAR"
        BuiltinId
    BuiltinAgdaLitString                     -> String
    "AGDALITSTRING"
        BuiltinId
    BuiltinAgdaLitQName                      -> String
    "AGDALITQNAME"
        BuiltinId
    BuiltinAgdaLitMeta                       -> String
    "AGDALITMETA"
        BuiltinId
    BuiltinAgdaClause                        -> String
    "AGDACLAUSE"
        BuiltinId
    BuiltinAgdaClauseClause                  -> String
    "AGDACLAUSECLAUSE"
        BuiltinId
    BuiltinAgdaClauseAbsurd                  -> String
    "AGDACLAUSEABSURD"
        BuiltinId
    BuiltinAgdaPattern                       -> String
    "AGDAPATTERN"
        BuiltinId
    BuiltinAgdaPatVar                        -> String
    "AGDAPATVAR"
        BuiltinId
    BuiltinAgdaPatCon                        -> String
    "AGDAPATCON"
        BuiltinId
    BuiltinAgdaPatDot                        -> String
    "AGDAPATDOT"
        BuiltinId
    BuiltinAgdaPatLit                        -> String
    "AGDAPATLIT"
        BuiltinId
    BuiltinAgdaPatProj                       -> String
    "AGDAPATPROJ"
        BuiltinId
    BuiltinAgdaPatAbsurd                     -> String
    "AGDAPATABSURD"
        BuiltinId
    BuiltinAgdaDefinitionFunDef              -> String
    "AGDADEFINITIONFUNDEF"
        BuiltinId
    BuiltinAgdaDefinitionDataDef             -> String
    "AGDADEFINITIONDATADEF"
        BuiltinId
    BuiltinAgdaDefinitionRecordDef           -> String
    "AGDADEFINITIONRECORDDEF"
        BuiltinId
    BuiltinAgdaDefinitionDataConstructor     -> String
    "AGDADEFINITIONDATACONSTRUCTOR"
        BuiltinId
    BuiltinAgdaDefinitionPostulate           -> String
    "AGDADEFINITIONPOSTULATE"
        BuiltinId
    BuiltinAgdaDefinitionPrimitive           -> String
    "AGDADEFINITIONPRIMITIVE"
        BuiltinId
    BuiltinAgdaDefinition                    -> String
    "AGDADEFINITION"
        BuiltinId
    BuiltinAgdaMeta                          -> String
    "AGDAMETA"
        BuiltinId
    BuiltinAgdaTCM                           -> String
    "AGDATCM"
        BuiltinId
    BuiltinAgdaTCMReturn                     -> String
    "AGDATCMRETURN"
        BuiltinId
    BuiltinAgdaTCMBind                       -> String
    "AGDATCMBIND"
        BuiltinId
    BuiltinAgdaTCMUnify                      -> String
    "AGDATCMUNIFY"
        BuiltinId
    BuiltinAgdaTCMTypeError                  -> String
    "AGDATCMTYPEERROR"
        BuiltinId
    BuiltinAgdaTCMInferType                  -> String
    "AGDATCMINFERTYPE"
        BuiltinId
    BuiltinAgdaTCMCheckType                  -> String
    "AGDATCMCHECKTYPE"
        BuiltinId
    BuiltinAgdaTCMNormalise                  -> String
    "AGDATCMNORMALISE"
        BuiltinId
    BuiltinAgdaTCMReduce                     -> String
    "AGDATCMREDUCE"
        BuiltinId
    BuiltinAgdaTCMCatchError                 -> String
    "AGDATCMCATCHERROR"
        BuiltinId
    BuiltinAgdaTCMGetContext                 -> String
    "AGDATCMGETCONTEXT"
        BuiltinId
    BuiltinAgdaTCMExtendContext              -> String
    "AGDATCMEXTENDCONTEXT"
        BuiltinId
    BuiltinAgdaTCMInContext                  -> String
    "AGDATCMINCONTEXT"
        BuiltinId
    BuiltinAgdaTCMFreshName                  -> String
    "AGDATCMFRESHNAME"
        BuiltinId
    BuiltinAgdaTCMDeclareDef                 -> String
    "AGDATCMDECLAREDEF"
        BuiltinId
    BuiltinAgdaTCMDeclarePostulate           -> String
    "AGDATCMDECLAREPOSTULATE"
        BuiltinId
    BuiltinAgdaTCMDeclareData                -> String
    "AGDATCMDECLAREDATA"
        BuiltinId
    BuiltinAgdaTCMDefineData                 -> String
    "AGDATCMDEFINEDATA"
        BuiltinId
    BuiltinAgdaTCMDefineFun                  -> String
    "AGDATCMDEFINEFUN"
        BuiltinId
    BuiltinAgdaTCMGetType                    -> String
    "AGDATCMGETTYPE"
        BuiltinId
    BuiltinAgdaTCMGetDefinition              -> String
    "AGDATCMGETDEFINITION"
        BuiltinId
    BuiltinAgdaTCMBlock                      -> String
    "AGDATCMBLOCK"
        BuiltinId
    BuiltinAgdaTCMCommit                     -> String
    "AGDATCMCOMMIT"
        BuiltinId
    BuiltinAgdaTCMQuoteTerm                  -> String
    "AGDATCMQUOTETERM"
        BuiltinId
    BuiltinAgdaTCMUnquoteTerm                -> String
    "AGDATCMUNQUOTETERM"
        BuiltinId
    BuiltinAgdaTCMQuoteOmegaTerm             -> String
    "AGDATCMQUOTEOMEGATERM"
        BuiltinId
    BuiltinAgdaTCMIsMacro                    -> String
    "AGDATCMISMACRO"
        BuiltinId
    BuiltinAgdaTCMWithNormalisation          -> String
    "AGDATCMWITHNORMALISATION"
        BuiltinId
    BuiltinAgdaTCMWithReconstructed          -> String
    "AGDATCMWITHRECONSTRUCTED"
        BuiltinId
    BuiltinAgdaTCMWithExpandLast             -> String
    "AGDATCMWITHEXPANDLAST"
        BuiltinId
    BuiltinAgdaTCMWithReduceDefs             -> String
    "AGDATCMWITHREDUCEDEFS"
        BuiltinId
    BuiltinAgdaTCMAskNormalisation           -> String
    "AGDATCMASKNORMALISATION"
        BuiltinId
    BuiltinAgdaTCMAskReconstructed           -> String
    "AGDATCMASKRECONSTRUCTED"
        BuiltinId
    BuiltinAgdaTCMAskExpandLast              -> String
    "AGDATCMASKEXPANDLAST"
        BuiltinId
    BuiltinAgdaTCMAskReduceDefs              -> String
    "AGDATCMASKREDUCEDEFS"
        BuiltinId
    BuiltinAgdaTCMFormatErrorParts           -> String
    "AGDATCMFORMATERRORPARTS"
        BuiltinId
    BuiltinAgdaTCMDebugPrint                 -> String
    "AGDATCMDEBUGPRINT"
        BuiltinId
    BuiltinAgdaTCMNoConstraints              -> String
    "AGDATCMNOCONSTRAINTS"
        BuiltinId
    BuiltinAgdaTCMWorkOnTypes                -> String
    "AGDATCMWORKONTYPES"
        BuiltinId
    BuiltinAgdaTCMRunSpeculative             -> String
    "AGDATCMRUNSPECULATIVE"
        BuiltinId
    BuiltinAgdaTCMExec                       -> String
    "AGDATCMEXEC"
        BuiltinId
    BuiltinAgdaTCMCheckFromString            -> String
    "AGDATCMCHECKFROMSTRING"
        BuiltinId
    BuiltinAgdaTCMGetInstances               -> String
    "AGDATCMGETINSTANCES"
        BuiltinId
    BuiltinAgdaTCMSolveInstances             -> String
    "AGDATCMSOLVEINSTANCES"
        BuiltinId
    BuiltinAgdaTCMPragmaForeign              -> String
    "AGDATCMPRAGMAFOREIGN"
        BuiltinId
    BuiltinAgdaTCMPragmaCompile              -> String
    "AGDATCMPRAGMACOMPILE"
        BuiltinId
    BuiltinAgdaBlocker                       -> String
    "AGDABLOCKER"
        BuiltinId
    BuiltinAgdaBlockerAny                    -> String
    "AGDABLOCKERANY"
        BuiltinId
    BuiltinAgdaBlockerAll                    -> String
    "AGDABLOCKERALL"
        BuiltinId
    BuiltinAgdaBlockerMeta                   -> String
    "AGDABLOCKERMETA"

    -- | 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 :: BuiltinId -> Bool
    isBuiltinNoDef :: BuiltinId -> Bool
    isBuiltinNoDef = [BuiltinId] -> BuiltinId -> Bool
    forall a. Ord a => [a] -> a -> Bool
    hasElem [BuiltinId]
    builtinsNoDef

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

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

    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,
      builtinIsOne,  builtinItIsOne, builtinIsOne1, builtinIsOne2, builtinIsOneEmpty,
      builtinSub, builtinSubIn,
      builtinEquiv, builtinEquivFun, builtinEquivProof,
      builtinTranspProof,
      builtinSizeUniv, builtinSize, builtinSizeLt,
      builtinSizeSuc, builtinSizeInf, builtinSizeMax,
      builtinInf, builtinSharp, builtinFlat,
      builtinEquality, builtinRefl, builtinRewrite, builtinLevelMax,
      builtinLevel, builtinLevelZero, builtinLevelSuc,
      builtinProp, builtinSet, builtinStrictSet,
      builtinPropOmega, builtinSetOmega, builtinSSetOmega,
      builtinLevelUniv,
      builtinIntervalUniv,
      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, builtinAgdaErrorPartPatt, 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, builtinAgdaTCMDeclareData, builtinAgdaTCMDefineData, builtinAgdaTCMDefineFun,
      builtinAgdaTCMGetType, builtinAgdaTCMGetDefinition,
      builtinAgdaTCMQuoteTerm, builtinAgdaTCMUnquoteTerm, builtinAgdaTCMQuoteOmegaTerm,
      builtinAgdaTCMCommit, builtinAgdaTCMIsMacro, builtinAgdaTCMBlock,
      builtinAgdaBlocker, builtinAgdaBlockerAll, builtinAgdaBlockerAny, builtinAgdaBlockerMeta,
      builtinAgdaTCMFormatErrorParts, builtinAgdaTCMDebugPrint,
      builtinAgdaTCMWithNormalisation, builtinAgdaTCMWithReconstructed,
      builtinAgdaTCMWithExpandLast, builtinAgdaTCMWithReduceDefs,
      builtinAgdaTCMAskNormalisation, builtinAgdaTCMAskReconstructed,
      builtinAgdaTCMAskExpandLast, builtinAgdaTCMAskReduceDefs,
      builtinAgdaTCMNoConstraints,
      builtinAgdaTCMWorkOnTypes,
      builtinAgdaTCMRunSpeculative,
      builtinAgdaTCMExec,
      builtinAgdaTCMCheckFromString,
      builtinAgdaTCMGetInstances,
      builtinAgdaTCMSolveInstances,
      builtinAgdaTCMPragmaForeign,
      builtinAgdaTCMPragmaCompile
      :: BuiltinId

    builtinNat :: BuiltinId
    builtinNat                               = BuiltinId
    BuiltinNat
    builtinSuc :: BuiltinId
    builtinSuc                               = BuiltinId
    BuiltinSuc
    builtinZero :: BuiltinId
    builtinZero                              = BuiltinId
    BuiltinZero
    builtinNatPlus :: BuiltinId
    builtinNatPlus                           = BuiltinId
    BuiltinNatPlus
    builtinNatMinus :: BuiltinId
    builtinNatMinus                          = BuiltinId
    BuiltinNatMinus
    builtinNatTimes :: BuiltinId
    builtinNatTimes                          = BuiltinId
    BuiltinNatTimes
    builtinNatDivSucAux :: BuiltinId
    builtinNatDivSucAux                      = BuiltinId
    BuiltinNatDivSucAux
    builtinNatModSucAux :: BuiltinId
    builtinNatModSucAux                      = BuiltinId
    BuiltinNatModSucAux
    builtinNatEquals :: BuiltinId
    builtinNatEquals                         = BuiltinId
    BuiltinNatEquals
    builtinNatLess :: BuiltinId
    builtinNatLess                           = BuiltinId
    BuiltinNatLess
    builtinWord64 :: BuiltinId
    builtinWord64                            = BuiltinId
    BuiltinWord64
    builtinInteger :: BuiltinId
    builtinInteger                           = BuiltinId
    BuiltinInteger
    builtinIntegerPos :: BuiltinId
    builtinIntegerPos                        = BuiltinId
    BuiltinIntegerPos
    builtinIntegerNegSuc :: BuiltinId
    builtinIntegerNegSuc                     = BuiltinId
    BuiltinIntegerNegSuc
    builtinFloat :: BuiltinId
    builtinFloat                             = BuiltinId
    BuiltinFloat
    builtinChar :: BuiltinId
    builtinChar                              = BuiltinId
    BuiltinChar
    builtinString :: BuiltinId
    builtinString                            = BuiltinId
    BuiltinString
    builtinUnit :: BuiltinId
    builtinUnit                              = BuiltinId
    BuiltinUnit
    builtinUnitUnit :: BuiltinId
    builtinUnitUnit                          = BuiltinId
    BuiltinUnitUnit
    builtinSigma :: BuiltinId
    builtinSigma                             = BuiltinId
    BuiltinSigma
    builtinBool :: BuiltinId
    builtinBool                              = BuiltinId
    BuiltinBool
    builtinTrue :: BuiltinId
    builtinTrue                              = BuiltinId
    BuiltinTrue
    builtinFalse :: BuiltinId
    builtinFalse                             = BuiltinId
    BuiltinFalse
    builtinList :: BuiltinId
    builtinList                              = BuiltinId
    BuiltinList
    builtinNil :: BuiltinId
    builtinNil                               = BuiltinId
    BuiltinNil
    builtinCons :: BuiltinId
    builtinCons                              = BuiltinId
    BuiltinCons
    builtinMaybe :: BuiltinId
    builtinMaybe                             = BuiltinId
    BuiltinMaybe
    builtinNothing :: BuiltinId
    builtinNothing                           = BuiltinId
    BuiltinNothing
    builtinJust :: BuiltinId
    builtinJust                              = BuiltinId
    BuiltinJust
    builtinIO :: BuiltinId
    builtinIO                                = BuiltinId
    BuiltinIO
    builtinPath :: BuiltinId
    builtinPath                              = BuiltinId
    BuiltinPath
    builtinPathP :: BuiltinId
    builtinPathP                             = BuiltinId
    BuiltinPathP
    builtinIntervalUniv :: BuiltinId
    builtinIntervalUniv                      = BuiltinId
    BuiltinIntervalUniv
    builtinInterval :: BuiltinId
    builtinInterval                          = BuiltinId
    BuiltinInterval
    builtinIZero :: BuiltinId
    builtinIZero                             = BuiltinId
    BuiltinIZero
    builtinIOne :: BuiltinId
    builtinIOne                              = BuiltinId
    BuiltinIOne
    builtinPartial :: BuiltinId
    builtinPartial                           = BuiltinId
    BuiltinPartial
    builtinPartialP :: BuiltinId
    builtinPartialP                          = BuiltinId
    BuiltinPartialP
    builtinIsOne :: BuiltinId
    builtinIsOne                             = BuiltinId
    BuiltinIsOne
    builtinItIsOne :: BuiltinId
    builtinItIsOne                           = BuiltinId
    BuiltinItIsOne
    builtinEquiv :: BuiltinId
    builtinEquiv                             = BuiltinId
    BuiltinEquiv
    builtinEquivFun :: BuiltinId
    builtinEquivFun                          = BuiltinId
    BuiltinEquivFun
    builtinEquivProof :: BuiltinId
    builtinEquivProof                        = BuiltinId
    BuiltinEquivProof
    builtinTranspProof :: BuiltinId
    builtinTranspProof                       = BuiltinId
    BuiltinTranspProof
    builtinIsOne1 :: BuiltinId
    builtinIsOne1                            = BuiltinId
    BuiltinIsOne1
    builtinIsOne2 :: BuiltinId
    builtinIsOne2                            = BuiltinId
    BuiltinIsOne2
    builtinIsOneEmpty :: BuiltinId
    builtinIsOneEmpty                        = BuiltinId
    BuiltinIsOneEmpty
    builtinSub :: BuiltinId
    builtinSub                               = BuiltinId
    BuiltinSub
    builtinSubIn :: BuiltinId
    builtinSubIn                             = BuiltinId
    BuiltinSubIn
    builtinSizeUniv :: BuiltinId
    builtinSizeUniv                          = BuiltinId
    BuiltinSizeUniv
    builtinSize :: BuiltinId
    builtinSize                              = BuiltinId
    BuiltinSize
    builtinSizeLt :: BuiltinId
    builtinSizeLt                            = BuiltinId
    BuiltinSizeLt
    builtinSizeSuc :: BuiltinId
    builtinSizeSuc                           = BuiltinId
    BuiltinSizeSuc
    builtinSizeInf :: BuiltinId
    builtinSizeInf                           = BuiltinId
    BuiltinSizeInf
    builtinSizeMax :: BuiltinId
    builtinSizeMax                           = BuiltinId
    BuiltinSizeMax
    builtinInf :: BuiltinId
    builtinInf                               = BuiltinId
    BuiltinInf
    builtinSharp :: BuiltinId
    builtinSharp                             = BuiltinId
    BuiltinSharp
    builtinFlat :: BuiltinId
    builtinFlat                              = BuiltinId
    BuiltinFlat
    builtinEquality :: BuiltinId
    builtinEquality                          = BuiltinId
    BuiltinEquality
    builtinRefl :: BuiltinId
    builtinRefl                              = BuiltinId
    BuiltinRefl
    builtinRewrite :: BuiltinId
    builtinRewrite                           = BuiltinId
    BuiltinRewrite
    builtinLevelMax :: BuiltinId
    builtinLevelMax                          = BuiltinId
    BuiltinLevelMax
    builtinLevel :: BuiltinId
    builtinLevel                             = BuiltinId
    BuiltinLevel
    builtinLevelZero :: BuiltinId
    builtinLevelZero                         = BuiltinId
    BuiltinLevelZero
    builtinLevelSuc :: BuiltinId
    builtinLevelSuc                          = BuiltinId
    BuiltinLevelSuc
    builtinProp :: BuiltinId
    builtinProp                              = BuiltinId
    BuiltinProp
    builtinSet :: BuiltinId
    builtinSet                               = BuiltinId
    BuiltinSet
    builtinStrictSet :: BuiltinId
    builtinStrictSet                         = BuiltinId
    BuiltinStrictSet
    builtinPropOmega :: BuiltinId
    builtinPropOmega                         = BuiltinId
    BuiltinPropOmega
    builtinSetOmega :: BuiltinId
    builtinSetOmega                          = BuiltinId
    BuiltinSetOmega
    builtinSSetOmega :: BuiltinId
    builtinSSetOmega                         = BuiltinId
    BuiltinSSetOmega
    builtinLevelUniv :: BuiltinId
    builtinLevelUniv                         = BuiltinId
    BuiltinLevelUniv
    builtinFromNat :: BuiltinId
    builtinFromNat                           = BuiltinId
    BuiltinFromNat
    builtinFromNeg :: BuiltinId
    builtinFromNeg                           = BuiltinId
    BuiltinFromNeg
    builtinFromString :: BuiltinId
    builtinFromString                        = BuiltinId
    BuiltinFromString
    builtinQName :: BuiltinId
    builtinQName                             = BuiltinId
    BuiltinQName
    builtinAgdaSort :: BuiltinId
    builtinAgdaSort                          = BuiltinId
    BuiltinAgdaSort
    builtinAgdaSortSet :: BuiltinId
    builtinAgdaSortSet                       = BuiltinId
    BuiltinAgdaSortSet
    builtinAgdaSortLit :: BuiltinId
    builtinAgdaSortLit                       = BuiltinId
    BuiltinAgdaSortLit
    builtinAgdaSortProp :: BuiltinId
    builtinAgdaSortProp                      = BuiltinId
    BuiltinAgdaSortProp
    builtinAgdaSortPropLit :: BuiltinId
    builtinAgdaSortPropLit                   = BuiltinId
    BuiltinAgdaSortPropLit
    builtinAgdaSortInf :: BuiltinId
    builtinAgdaSortInf                       = BuiltinId
    BuiltinAgdaSortInf
    builtinAgdaSortUnsupported :: BuiltinId
    builtinAgdaSortUnsupported               = BuiltinId
    BuiltinAgdaSortUnsupported
    builtinHiding :: BuiltinId
    builtinHiding                            = BuiltinId
    BuiltinHiding
    builtinHidden :: BuiltinId
    builtinHidden                            = BuiltinId
    BuiltinHidden
    builtinInstance :: BuiltinId
    builtinInstance                          = BuiltinId
    BuiltinInstance
    builtinVisible :: BuiltinId
    builtinVisible                           = BuiltinId
    BuiltinVisible
    builtinRelevance :: BuiltinId
    builtinRelevance                         = BuiltinId
    BuiltinRelevance
    builtinRelevant :: BuiltinId
    builtinRelevant                          = BuiltinId
    BuiltinRelevant
    builtinIrrelevant :: BuiltinId
    builtinIrrelevant                        = BuiltinId
    BuiltinIrrelevant
    builtinQuantity :: BuiltinId
    builtinQuantity                          = BuiltinId
    BuiltinQuantity
    builtinQuantity0 :: BuiltinId
    builtinQuantity0                         = BuiltinId
    BuiltinQuantity0
    builtinQuantityω :: BuiltinId
    builtinQuantityω                         = BuiltinId
    BuiltinQuantityω
    builtinModality :: BuiltinId
    builtinModality                          = BuiltinId
    BuiltinModality
    builtinModalityConstructor :: BuiltinId
    builtinModalityConstructor               = BuiltinId
    BuiltinModalityConstructor
    builtinAssoc :: BuiltinId
    builtinAssoc                             = BuiltinId
    BuiltinAssoc
    builtinAssocLeft :: BuiltinId
    builtinAssocLeft                         = BuiltinId
    BuiltinAssocLeft
    builtinAssocRight :: BuiltinId
    builtinAssocRight                        = BuiltinId
    BuiltinAssocRight
    builtinAssocNon :: BuiltinId
    builtinAssocNon                          = BuiltinId
    BuiltinAssocNon
    builtinPrecedence :: BuiltinId
    builtinPrecedence                        = BuiltinId
    BuiltinPrecedence
    builtinPrecRelated :: BuiltinId
    builtinPrecRelated                       = BuiltinId
    BuiltinPrecRelated
    builtinPrecUnrelated :: BuiltinId
    builtinPrecUnrelated                     = BuiltinId
    BuiltinPrecUnrelated
    builtinFixity :: BuiltinId
    builtinFixity                            = BuiltinId
    BuiltinFixity
    builtinFixityFixity :: BuiltinId
    builtinFixityFixity                      = BuiltinId
    BuiltinFixityFixity
    builtinArg :: BuiltinId
    builtinArg                               = BuiltinId
    BuiltinArg
    builtinArgInfo :: BuiltinId
    builtinArgInfo                           = BuiltinId
    BuiltinArgInfo
    builtinArgArgInfo :: BuiltinId
    builtinArgArgInfo                        = BuiltinId
    BuiltinArgArgInfo
    builtinArgArg :: BuiltinId
    builtinArgArg                            = BuiltinId
    BuiltinArgArg
    builtinAbs :: BuiltinId
    builtinAbs                               = BuiltinId
    BuiltinAbs
    builtinAbsAbs :: BuiltinId
    builtinAbsAbs                            = BuiltinId
    BuiltinAbsAbs
    builtinAgdaTerm :: BuiltinId
    builtinAgdaTerm                          = BuiltinId
    BuiltinAgdaTerm
    builtinAgdaTermVar :: BuiltinId
    builtinAgdaTermVar                       = BuiltinId
    BuiltinAgdaTermVar
    builtinAgdaTermLam :: BuiltinId
    builtinAgdaTermLam                       = BuiltinId
    BuiltinAgdaTermLam
    builtinAgdaTermExtLam :: BuiltinId
    builtinAgdaTermExtLam                    = BuiltinId
    BuiltinAgdaTermExtLam
    builtinAgdaTermDef :: BuiltinId
    builtinAgdaTermDef                       = BuiltinId
    BuiltinAgdaTermDef
    builtinAgdaTermCon :: BuiltinId
    builtinAgdaTermCon                       = BuiltinId
    BuiltinAgdaTermCon
    builtinAgdaTermPi :: BuiltinId
    builtinAgdaTermPi                        = BuiltinId
    BuiltinAgdaTermPi
    builtinAgdaTermSort :: BuiltinId
    builtinAgdaTermSort                      = BuiltinId
    BuiltinAgdaTermSort
    builtinAgdaTermLit :: BuiltinId
    builtinAgdaTermLit                       = BuiltinId
    BuiltinAgdaTermLit
    builtinAgdaTermUnsupported :: BuiltinId
    builtinAgdaTermUnsupported               = BuiltinId
    BuiltinAgdaTermUnsupported
    builtinAgdaTermMeta :: BuiltinId
    builtinAgdaTermMeta                      = BuiltinId
    BuiltinAgdaTermMeta
    builtinAgdaErrorPart :: BuiltinId
    builtinAgdaErrorPart                     = BuiltinId
    BuiltinAgdaErrorPart
    builtinAgdaErrorPartString :: BuiltinId
    builtinAgdaErrorPartString               = BuiltinId
    BuiltinAgdaErrorPartString
    builtinAgdaErrorPartTerm :: BuiltinId
    builtinAgdaErrorPartTerm                 = BuiltinId
    BuiltinAgdaErrorPartTerm
    builtinAgdaErrorPartPatt :: BuiltinId
    builtinAgdaErrorPartPatt                 = BuiltinId
    BuiltinAgdaErrorPartPatt
    builtinAgdaErrorPartName :: BuiltinId
    builtinAgdaErrorPartName                 = BuiltinId
    BuiltinAgdaErrorPartName
    builtinAgdaLiteral :: BuiltinId
    builtinAgdaLiteral                       = BuiltinId
    BuiltinAgdaLiteral
    builtinAgdaLitNat :: BuiltinId
    builtinAgdaLitNat                        = BuiltinId
    BuiltinAgdaLitNat
    builtinAgdaLitWord64 :: BuiltinId
    builtinAgdaLitWord64                     = BuiltinId
    BuiltinAgdaLitWord64
    builtinAgdaLitFloat :: BuiltinId
    builtinAgdaLitFloat                      = BuiltinId
    BuiltinAgdaLitFloat
    builtinAgdaLitChar :: BuiltinId
    builtinAgdaLitChar                       = BuiltinId
    BuiltinAgdaLitChar
    builtinAgdaLitString :: BuiltinId
    builtinAgdaLitString                     = BuiltinId
    BuiltinAgdaLitString
    builtinAgdaLitQName :: BuiltinId
    builtinAgdaLitQName                      = BuiltinId
    BuiltinAgdaLitQName
    builtinAgdaLitMeta :: BuiltinId
    builtinAgdaLitMeta                       = BuiltinId
    BuiltinAgdaLitMeta
    builtinAgdaClause :: BuiltinId
    builtinAgdaClause                        = BuiltinId
    BuiltinAgdaClause
    builtinAgdaClauseClause :: BuiltinId
    builtinAgdaClauseClause                  = BuiltinId
    BuiltinAgdaClauseClause
    builtinAgdaClauseAbsurd :: BuiltinId
    builtinAgdaClauseAbsurd                  = BuiltinId
    BuiltinAgdaClauseAbsurd
    builtinAgdaPattern :: BuiltinId
    builtinAgdaPattern                       = BuiltinId
    BuiltinAgdaPattern
    builtinAgdaPatVar :: BuiltinId
    builtinAgdaPatVar                        = BuiltinId
    BuiltinAgdaPatVar
    builtinAgdaPatCon :: BuiltinId
    builtinAgdaPatCon                        = BuiltinId
    BuiltinAgdaPatCon
    builtinAgdaPatDot :: BuiltinId
    builtinAgdaPatDot                        = BuiltinId
    BuiltinAgdaPatDot
    builtinAgdaPatLit :: BuiltinId
    builtinAgdaPatLit                        = BuiltinId
    BuiltinAgdaPatLit
    builtinAgdaPatProj :: BuiltinId
    builtinAgdaPatProj                       = BuiltinId
    BuiltinAgdaPatProj
    builtinAgdaPatAbsurd :: BuiltinId
    builtinAgdaPatAbsurd                     = BuiltinId
    BuiltinAgdaPatAbsurd
    builtinAgdaDefinitionFunDef :: BuiltinId
    builtinAgdaDefinitionFunDef              = BuiltinId
    BuiltinAgdaDefinitionFunDef
    builtinAgdaDefinitionDataDef :: BuiltinId
    builtinAgdaDefinitionDataDef             = BuiltinId
    BuiltinAgdaDefinitionDataDef
    builtinAgdaDefinitionRecordDef :: BuiltinId
    builtinAgdaDefinitionRecordDef           = BuiltinId
    BuiltinAgdaDefinitionRecordDef
    builtinAgdaDefinitionDataConstructor :: BuiltinId
    builtinAgdaDefinitionDataConstructor     = BuiltinId
    BuiltinAgdaDefinitionDataConstructor
    builtinAgdaDefinitionPostulate :: BuiltinId
    builtinAgdaDefinitionPostulate           = BuiltinId
    BuiltinAgdaDefinitionPostulate
    builtinAgdaDefinitionPrimitive :: BuiltinId
    builtinAgdaDefinitionPrimitive           = BuiltinId
    BuiltinAgdaDefinitionPrimitive
    builtinAgdaDefinition :: BuiltinId
    builtinAgdaDefinition                    = BuiltinId
    BuiltinAgdaDefinition
    builtinAgdaMeta :: BuiltinId
    builtinAgdaMeta                          = BuiltinId
    BuiltinAgdaMeta
    builtinAgdaTCM :: BuiltinId
    builtinAgdaTCM                           = BuiltinId
    BuiltinAgdaTCM
    builtinAgdaTCMReturn :: BuiltinId
    builtinAgdaTCMReturn                     = BuiltinId
    BuiltinAgdaTCMReturn
    builtinAgdaTCMBind :: BuiltinId
    builtinAgdaTCMBind                       = BuiltinId
    BuiltinAgdaTCMBind
    builtinAgdaTCMUnify :: BuiltinId
    builtinAgdaTCMUnify                      = BuiltinId
    BuiltinAgdaTCMUnify
    builtinAgdaTCMTypeError :: BuiltinId
    builtinAgdaTCMTypeError                  = BuiltinId
    BuiltinAgdaTCMTypeError
    builtinAgdaTCMInferType :: BuiltinId
    builtinAgdaTCMInferType                  = BuiltinId
    BuiltinAgdaTCMInferType
    builtinAgdaTCMCheckType :: BuiltinId
    builtinAgdaTCMCheckType                  = BuiltinId
    BuiltinAgdaTCMCheckType
    builtinAgdaTCMNormalise :: BuiltinId
    builtinAgdaTCMNormalise                  = BuiltinId
    BuiltinAgdaTCMNormalise
    builtinAgdaTCMReduce :: BuiltinId
    builtinAgdaTCMReduce                     = BuiltinId
    BuiltinAgdaTCMReduce
    builtinAgdaTCMCatchError :: BuiltinId
    builtinAgdaTCMCatchError                 = BuiltinId
    BuiltinAgdaTCMCatchError
    builtinAgdaTCMGetContext :: BuiltinId
    builtinAgdaTCMGetContext                 = BuiltinId
    BuiltinAgdaTCMGetContext
    builtinAgdaTCMExtendContext :: BuiltinId
    builtinAgdaTCMExtendContext              = BuiltinId
    BuiltinAgdaTCMExtendContext
    builtinAgdaTCMInContext :: BuiltinId
    builtinAgdaTCMInContext                  = BuiltinId
    BuiltinAgdaTCMInContext
    builtinAgdaTCMFreshName :: BuiltinId
    builtinAgdaTCMFreshName                  = BuiltinId
    BuiltinAgdaTCMFreshName
    builtinAgdaTCMDeclareDef :: BuiltinId
    builtinAgdaTCMDeclareDef                 = BuiltinId
    BuiltinAgdaTCMDeclareDef
    builtinAgdaTCMDeclarePostulate :: BuiltinId
    builtinAgdaTCMDeclarePostulate           = BuiltinId
    BuiltinAgdaTCMDeclarePostulate
    builtinAgdaTCMDeclareData :: BuiltinId
    builtinAgdaTCMDeclareData                = BuiltinId
    BuiltinAgdaTCMDeclareData
    builtinAgdaTCMDefineData :: BuiltinId
    builtinAgdaTCMDefineData                 = BuiltinId
    BuiltinAgdaTCMDefineData
    builtinAgdaTCMDefineFun :: BuiltinId
    builtinAgdaTCMDefineFun                  = BuiltinId
    BuiltinAgdaTCMDefineFun
    builtinAgdaTCMGetType :: BuiltinId
    builtinAgdaTCMGetType                    = BuiltinId
    BuiltinAgdaTCMGetType
    builtinAgdaTCMGetDefinition :: BuiltinId
    builtinAgdaTCMGetDefinition              = BuiltinId
    BuiltinAgdaTCMGetDefinition
    builtinAgdaTCMBlock :: BuiltinId
    builtinAgdaTCMBlock                      = BuiltinId
    BuiltinAgdaTCMBlock
    builtinAgdaTCMCommit :: BuiltinId
    builtinAgdaTCMCommit                     = BuiltinId
    BuiltinAgdaTCMCommit
    builtinAgdaTCMQuoteTerm :: BuiltinId
    builtinAgdaTCMQuoteTerm                  = BuiltinId
    BuiltinAgdaTCMQuoteTerm
    builtinAgdaTCMUnquoteTerm :: BuiltinId
    builtinAgdaTCMUnquoteTerm                = BuiltinId
    BuiltinAgdaTCMUnquoteTerm
    builtinAgdaTCMQuoteOmegaTerm :: BuiltinId
    builtinAgdaTCMQuoteOmegaTerm             = BuiltinId
    BuiltinAgdaTCMQuoteOmegaTerm
    builtinAgdaTCMIsMacro :: BuiltinId
    builtinAgdaTCMIsMacro                    = BuiltinId
    BuiltinAgdaTCMIsMacro
    builtinAgdaTCMWithNormalisation :: BuiltinId
    builtinAgdaTCMWithNormalisation          = BuiltinId
    BuiltinAgdaTCMWithNormalisation
    builtinAgdaTCMWithReconstructed :: BuiltinId
    builtinAgdaTCMWithReconstructed          = BuiltinId
    BuiltinAgdaTCMWithReconstructed
    builtinAgdaTCMWithExpandLast :: BuiltinId
    builtinAgdaTCMWithExpandLast             = BuiltinId
    BuiltinAgdaTCMWithExpandLast
    builtinAgdaTCMWithReduceDefs :: BuiltinId
    builtinAgdaTCMWithReduceDefs             = BuiltinId
    BuiltinAgdaTCMWithReduceDefs
    builtinAgdaTCMAskNormalisation :: BuiltinId
    builtinAgdaTCMAskNormalisation           = BuiltinId
    BuiltinAgdaTCMAskNormalisation
    builtinAgdaTCMAskReconstructed :: BuiltinId
    builtinAgdaTCMAskReconstructed           = BuiltinId
    BuiltinAgdaTCMAskReconstructed
    builtinAgdaTCMAskExpandLast :: BuiltinId
    builtinAgdaTCMAskExpandLast              = BuiltinId
    BuiltinAgdaTCMAskExpandLast
    builtinAgdaTCMAskReduceDefs :: BuiltinId
    builtinAgdaTCMAskReduceDefs              = BuiltinId
    BuiltinAgdaTCMAskReduceDefs
    builtinAgdaTCMFormatErrorParts :: BuiltinId
    builtinAgdaTCMFormatErrorParts           = BuiltinId
    BuiltinAgdaTCMFormatErrorParts
    builtinAgdaTCMDebugPrint :: BuiltinId
    builtinAgdaTCMDebugPrint                 = BuiltinId
    BuiltinAgdaTCMDebugPrint
    builtinAgdaTCMNoConstraints :: BuiltinId
    builtinAgdaTCMNoConstraints              = BuiltinId
    BuiltinAgdaTCMNoConstraints
    builtinAgdaTCMWorkOnTypes :: BuiltinId
    builtinAgdaTCMWorkOnTypes                = BuiltinId
    BuiltinAgdaTCMWorkOnTypes
    builtinAgdaTCMRunSpeculative :: BuiltinId
    builtinAgdaTCMRunSpeculative             = BuiltinId
    BuiltinAgdaTCMRunSpeculative
    builtinAgdaTCMExec :: BuiltinId
    builtinAgdaTCMExec                       = BuiltinId
    BuiltinAgdaTCMExec
    builtinAgdaTCMCheckFromString :: BuiltinId
    builtinAgdaTCMCheckFromString            = BuiltinId
    BuiltinAgdaTCMCheckFromString
    builtinAgdaTCMGetInstances :: BuiltinId
    builtinAgdaTCMGetInstances               = BuiltinId
    BuiltinAgdaTCMGetInstances
    builtinAgdaTCMSolveInstances :: BuiltinId
    builtinAgdaTCMSolveInstances             = BuiltinId
    BuiltinAgdaTCMSolveInstances
    builtinAgdaTCMPragmaForeign :: BuiltinId
    builtinAgdaTCMPragmaForeign              = BuiltinId
    BuiltinAgdaTCMPragmaForeign
    builtinAgdaTCMPragmaCompile :: BuiltinId
    builtinAgdaTCMPragmaCompile              = BuiltinId
    BuiltinAgdaTCMPragmaCompile
    builtinAgdaBlocker :: BuiltinId
    builtinAgdaBlocker                       = BuiltinId
    BuiltinAgdaBlocker
    builtinAgdaBlockerAny :: BuiltinId
    builtinAgdaBlockerAny                    = BuiltinId
    BuiltinAgdaBlockerAny
    builtinAgdaBlockerAll :: BuiltinId
    builtinAgdaBlockerAll                    = BuiltinId
    BuiltinAgdaBlockerAll
    builtinAgdaBlockerMeta :: BuiltinId
    builtinAgdaBlockerMeta                   = BuiltinId
    BuiltinAgdaBlockerMeta

    -- | Lookup a builtin by the string used in the @BUILTIN@ pragma.
    builtinById :: String -> Maybe BuiltinId
    builtinById :: String -> Maybe BuiltinId
    builtinById = (String -> Map String BuiltinId -> Maybe BuiltinId)
    -> Map String BuiltinId -> String -> Maybe BuiltinId
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip String -> Map String BuiltinId -> Maybe BuiltinId
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Map String BuiltinId
    m where
      m :: Map String BuiltinId
    m = [(String, BuiltinId)] -> Map String BuiltinId
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(BuiltinId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId BuiltinId
    x, BuiltinId
    x) | BuiltinId
    x <- [(BuiltinId
    forall a. Bounded a => a
    minBound :: BuiltinId)..]]

    -- * Primitives

    -- | A primitive name, defined by the @primitive@ block.
    data PrimitiveId
      -- Cubical
      = PrimIMin
      | PrimIMax
      | PrimINeg
      | PrimPartial
      | PrimPartialP
      | PrimSubOut
      | PrimGlue
      | Prim_glue
      | Prim_unglue
      | Prim_glueU
      | Prim_unglueU
      | PrimFaceForall
      | PrimComp
      | PrimPOr
      | PrimTrans
      | PrimHComp
      --  Integer
      | PrimShowInteger
      -- Natural
      | PrimNatPlus
      | PrimNatMinus
      | PrimNatTimes
      | PrimNatDivSucAux
      | PrimNatModSucAux
      | PrimNatEquality
      | PrimNatLess
      | PrimShowNat
      -- Word64
      | PrimWord64FromNat
      | PrimWord64ToNat
      | PrimWord64ToNatInjective
      -- Level
      | PrimLevelZero
      | PrimLevelSuc
      | PrimLevelMax
      -- Float
      | PrimFloatEquality
      | PrimFloatInequality
      | PrimFloatLess
      | PrimFloatIsInfinite
      | PrimFloatIsNaN
      | PrimFloatIsNegativeZero
      | PrimFloatIsSafeInteger
      | PrimFloatToWord64
      | PrimFloatToWord64Injective
      | PrimNatToFloat
      | PrimIntToFloat
      | PrimFloatRound
      | PrimFloatFloor
      | PrimFloatCeiling
      | PrimFloatToRatio
      | PrimRatioToFloat
      | PrimFloatDecode
      | PrimFloatEncode
      | PrimShowFloat
      | PrimFloatPlus
      | PrimFloatMinus
      | PrimFloatTimes
      | PrimFloatNegate
      | PrimFloatDiv
      | PrimFloatPow
      | PrimFloatSqrt
      | PrimFloatExp
      | PrimFloatLog
      | PrimFloatSin
      | PrimFloatCos
      | PrimFloatTan
      | PrimFloatASin
      | PrimFloatACos
      | PrimFloatATan
      | PrimFloatATan2
      | PrimFloatSinh
      | PrimFloatCosh
      | PrimFloatTanh
      | PrimFloatASinh
      | PrimFloatACosh
      | PrimFloatATanh
      -- Character
      | PrimCharEquality
      | PrimIsLower
      | PrimIsDigit
      | PrimIsAlpha
      | PrimIsSpace
      | PrimIsAscii
      | PrimIsLatin1
      | PrimIsPrint
      | PrimIsHexDigit
      | PrimToUpper
      | PrimToLower
      | PrimCharToNat
      | PrimCharToNatInjective
      | PrimNatToChar
      | PrimShowChar
      -- String
      | PrimStringToList
      | PrimStringToListInjective
      | PrimStringFromList
      | PrimStringFromListInjective
      | PrimStringAppend
      | PrimStringEquality
      | PrimShowString
      | PrimStringUncons
      -- "Other stuff"
      | PrimErase
      | PrimEraseEquality
      | PrimForce
      | PrimForceLemma
      | PrimQNameEquality
      | PrimQNameLess
      | PrimShowQName
      | PrimQNameFixity
      | PrimQNameToWord64s
      | PrimQNameToWord64sInjective
      | PrimMetaEquality
      | PrimMetaLess
      | PrimShowMeta
      | PrimMetaToNat
      | PrimMetaToNatInjective
      | PrimLockUniv
      deriving (Int -> PrimitiveId -> ShowS
    [PrimitiveId] -> ShowS
    PrimitiveId -> String
    (Int -> PrimitiveId -> ShowS)
    -> (PrimitiveId -> String)
    -> ([PrimitiveId] -> ShowS)
    -> Show PrimitiveId
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> PrimitiveId -> ShowS
    showsPrec :: Int -> PrimitiveId -> ShowS
    $cshow :: PrimitiveId -> String
    show :: PrimitiveId -> String
    $cshowList :: [PrimitiveId] -> ShowS
    showList :: [PrimitiveId] -> ShowS
    Show, PrimitiveId -> PrimitiveId -> Bool
    (PrimitiveId -> PrimitiveId -> Bool)
    -> (PrimitiveId -> PrimitiveId -> Bool) -> Eq PrimitiveId
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: PrimitiveId -> PrimitiveId -> Bool
    == :: PrimitiveId -> PrimitiveId -> Bool
    $c/= :: PrimitiveId -> PrimitiveId -> Bool
    /= :: PrimitiveId -> PrimitiveId -> Bool
    Eq, Eq PrimitiveId
    Eq PrimitiveId =>
    (PrimitiveId -> PrimitiveId -> Ordering)
    -> (PrimitiveId -> PrimitiveId -> Bool)
    -> (PrimitiveId -> PrimitiveId -> Bool)
    -> (PrimitiveId -> PrimitiveId -> Bool)
    -> (PrimitiveId -> PrimitiveId -> Bool)
    -> (PrimitiveId -> PrimitiveId -> PrimitiveId)
    -> (PrimitiveId -> PrimitiveId -> PrimitiveId)
    -> Ord PrimitiveId
    PrimitiveId -> PrimitiveId -> Bool
    PrimitiveId -> PrimitiveId -> Ordering
    PrimitiveId -> PrimitiveId -> PrimitiveId
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: PrimitiveId -> PrimitiveId -> Ordering
    compare :: PrimitiveId -> PrimitiveId -> Ordering
    $c< :: PrimitiveId -> PrimitiveId -> Bool
    < :: PrimitiveId -> PrimitiveId -> Bool
    $c<= :: PrimitiveId -> PrimitiveId -> Bool
    <= :: PrimitiveId -> PrimitiveId -> Bool
    $c> :: PrimitiveId -> PrimitiveId -> Bool
    > :: PrimitiveId -> PrimitiveId -> Bool
    $c>= :: PrimitiveId -> PrimitiveId -> Bool
    >= :: PrimitiveId -> PrimitiveId -> Bool
    $cmax :: PrimitiveId -> PrimitiveId -> PrimitiveId
    max :: PrimitiveId -> PrimitiveId -> PrimitiveId
    $cmin :: PrimitiveId -> PrimitiveId -> PrimitiveId
    min :: PrimitiveId -> PrimitiveId -> PrimitiveId
    Ord, PrimitiveId
    PrimitiveId -> PrimitiveId -> Bounded PrimitiveId
    forall a. a -> a -> Bounded a
    $cminBound :: PrimitiveId
    minBound :: PrimitiveId
    $cmaxBound :: PrimitiveId
    maxBound :: PrimitiveId
    Bounded, Int -> PrimitiveId
    PrimitiveId -> Int
    PrimitiveId -> [PrimitiveId]
    PrimitiveId -> PrimitiveId
    PrimitiveId -> PrimitiveId -> [PrimitiveId]
    PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
    (PrimitiveId -> PrimitiveId)
    -> (PrimitiveId -> PrimitiveId)
    -> (Int -> PrimitiveId)
    -> (PrimitiveId -> Int)
    -> (PrimitiveId -> [PrimitiveId])
    -> (PrimitiveId -> PrimitiveId -> [PrimitiveId])
    -> (PrimitiveId -> PrimitiveId -> [PrimitiveId])
    -> (PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId])
    -> Enum PrimitiveId
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    $csucc :: PrimitiveId -> PrimitiveId
    succ :: PrimitiveId -> PrimitiveId
    $cpred :: PrimitiveId -> PrimitiveId
    pred :: PrimitiveId -> PrimitiveId
    $ctoEnum :: Int -> PrimitiveId
    toEnum :: Int -> PrimitiveId
    $cfromEnum :: PrimitiveId -> Int
    fromEnum :: PrimitiveId -> Int
    $cenumFrom :: PrimitiveId -> [PrimitiveId]
    enumFrom :: PrimitiveId -> [PrimitiveId]
    $cenumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
    enumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
    $cenumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
    enumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId]
    $cenumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
    enumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]
    Enum, (forall x. PrimitiveId -> Rep PrimitiveId x)
    -> (forall x. Rep PrimitiveId x -> PrimitiveId)
    -> Generic PrimitiveId
    forall x. Rep PrimitiveId x -> PrimitiveId
    forall x. PrimitiveId -> Rep PrimitiveId x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. PrimitiveId -> Rep PrimitiveId x
    from :: forall x. PrimitiveId -> Rep PrimitiveId x
    $cto :: forall x. Rep PrimitiveId x -> PrimitiveId
    to :: forall x. Rep PrimitiveId x -> PrimitiveId
    Generic)

    instance NFData PrimitiveId

    instance Hashable PrimitiveId where
      Int
    s hashWithSalt :: Int -> PrimitiveId -> Int
    `hashWithSalt` PrimitiveId
    b = Int
    s Int -> Int -> Int
    forall a. Hashable a => Int -> a -> Int
    `hashWithSalt` PrimitiveId -> Int
    forall a. Enum a => a -> Int
    fromEnum PrimitiveId
    b

    instance KillRange PrimitiveId where
      killRange :: PrimitiveId -> PrimitiveId
    killRange = PrimitiveId -> PrimitiveId
    forall a. a -> a
    id

    instance Pretty PrimitiveId where
      pretty :: PrimitiveId -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    text (String -> Doc) -> (PrimitiveId -> String) -> PrimitiveId -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId

    instance IsBuiltin PrimitiveId where
      someBuiltin :: PrimitiveId -> SomeBuiltin
    someBuiltin = PrimitiveId -> SomeBuiltin
    PrimitiveName

      getBuiltinId :: PrimitiveId -> String
    getBuiltinId = \case
        -- Cubical
        PrimitiveId
    PrimIMin                              -> String
    "primIMin"
        PrimitiveId
    PrimIMax                              -> String
    "primIMax"
        PrimitiveId
    PrimINeg                              -> String
    "primINeg"
        PrimitiveId
    PrimPartial                           -> String
    "primPartial"
        PrimitiveId
    PrimPartialP                          -> String
    "primPartialP"
        PrimitiveId
    PrimSubOut                            -> String
    "primSubOut"
        PrimitiveId
    PrimGlue                              -> String
    "primGlue"
        PrimitiveId
    Prim_glue                             -> String
    "prim^glue"
        PrimitiveId
    Prim_unglue                           -> String
    "prim^unglue"
        PrimitiveId
    Prim_glueU                            -> String
    "prim^glueU"
        PrimitiveId
    Prim_unglueU                          -> String
    "prim^unglueU"
        PrimitiveId
    PrimFaceForall                        -> String
    "primFaceForall"
        PrimitiveId
    PrimComp                              -> String
    "primComp"
        PrimitiveId
    PrimPOr                               -> String
    "primPOr"
        PrimitiveId
    PrimTrans                             -> String
    "primTransp"
        PrimitiveId
    PrimHComp                             -> String
    "primHComp"
        --  Integer
        PrimitiveId
    PrimShowInteger                       -> String
    "primShowInteger"
        -- Natural
        PrimitiveId
    PrimNatPlus                           -> String
    "primNatPlus"
        PrimitiveId
    PrimNatMinus                          -> String
    "primNatMinus"
        PrimitiveId
    PrimNatTimes                          -> String
    "primNatTimes"
        PrimitiveId
    PrimNatDivSucAux                      -> String
    "primNatDivSucAux"
        PrimitiveId
    PrimNatModSucAux                      -> String
    "primNatModSucAux"
        PrimitiveId
    PrimNatEquality                       -> String
    "primNatEquality"
        PrimitiveId
    PrimNatLess                           -> String
    "primNatLess"
        PrimitiveId
    PrimShowNat                           -> String
    "primShowNat"
        -- Word64
        PrimitiveId
    PrimWord64FromNat                     -> String
    "primWord64FromNat"
        PrimitiveId
    PrimWord64ToNat                       -> String
    "primWord64ToNat"
        PrimitiveId
    PrimWord64ToNatInjective              -> String
    "primWord64ToNatInjective"
        -- Level
        PrimitiveId
    PrimLevelZero                         -> String
    "primLevelZero"
        PrimitiveId
    PrimLevelSuc                          -> String
    "primLevelSuc"
        PrimitiveId
    PrimLevelMax                          -> String
    "primLevelMax"
        -- Float
        PrimitiveId
    PrimFloatEquality                     -> String
    "primFloatEquality"
        PrimitiveId
    PrimFloatInequality                   -> String
    "primFloatInequality"
        PrimitiveId
    PrimFloatLess                         -> String
    "primFloatLess"
        PrimitiveId
    PrimFloatIsInfinite                   -> String
    "primFloatIsInfinite"
        PrimitiveId
    PrimFloatIsNaN                        -> String
    "primFloatIsNaN"
        PrimitiveId
    PrimFloatIsNegativeZero               -> String
    "primFloatIsNegativeZero"
        PrimitiveId
    PrimFloatIsSafeInteger                -> String
    "primFloatIsSafeInteger"
        PrimitiveId
    PrimFloatToWord64                     -> String
    "primFloatToWord64"
        PrimitiveId
    PrimFloatToWord64Injective            -> String
    "primFloatToWord64Injective"
        PrimitiveId
    PrimNatToFloat                        -> String
    "primNatToFloat"
        PrimitiveId
    PrimIntToFloat                        -> String
    "primIntToFloat"
        PrimitiveId
    PrimFloatRound                        -> String
    "primFloatRound"
        PrimitiveId
    PrimFloatFloor                        -> String
    "primFloatFloor"
        PrimitiveId
    PrimFloatCeiling                      -> String
    "primFloatCeiling"
        PrimitiveId
    PrimFloatToRatio                      -> String
    "primFloatToRatio"
        PrimitiveId
    PrimRatioToFloat                      -> String
    "primRatioToFloat"
        PrimitiveId
    PrimFloatDecode                       -> String
    "primFloatDecode"
        PrimitiveId
    PrimFloatEncode                       -> String
    "primFloatEncode"
        PrimitiveId
    PrimShowFloat                         -> String
    "primShowFloat"
        PrimitiveId
    PrimFloatPlus                         -> String
    "primFloatPlus"
        PrimitiveId
    PrimFloatMinus                        -> String
    "primFloatMinus"
        PrimitiveId
    PrimFloatTimes                        -> String
    "primFloatTimes"
        PrimitiveId
    PrimFloatNegate                       -> String
    "primFloatNegate"
        PrimitiveId
    PrimFloatDiv                          -> String
    "primFloatDiv"
        PrimitiveId
    PrimFloatPow                          -> String
    "primFloatPow"
        PrimitiveId
    PrimFloatSqrt                         -> String
    "primFloatSqrt"
        PrimitiveId
    PrimFloatExp                          -> String
    "primFloatExp"
        PrimitiveId
    PrimFloatLog                          -> String
    "primFloatLog"
        PrimitiveId
    PrimFloatSin                          -> String
    "primFloatSin"
        PrimitiveId
    PrimFloatCos                          -> String
    "primFloatCos"
        PrimitiveId
    PrimFloatTan                          -> String
    "primFloatTan"
        PrimitiveId
    PrimFloatASin                         -> String
    "primFloatASin"
        PrimitiveId
    PrimFloatACos                         -> String
    "primFloatACos"
        PrimitiveId
    PrimFloatATan                         -> String
    "primFloatATan"
        PrimitiveId
    PrimFloatATan2                        -> String
    "primFloatATan2"
        PrimitiveId
    PrimFloatSinh                         -> String
    "primFloatSinh"
        PrimitiveId
    PrimFloatCosh                         -> String
    "primFloatCosh"
        PrimitiveId
    PrimFloatTanh                         -> String
    "primFloatTanh"
        PrimitiveId
    PrimFloatASinh                        -> String
    "primFloatASinh"
        PrimitiveId
    PrimFloatACosh                        -> String
    "primFloatACosh"
        PrimitiveId
    PrimFloatATanh                        -> String
    "primFloatATanh"
        -- Character
        PrimitiveId
    PrimCharEquality                      -> String
    "primCharEquality"
        PrimitiveId
    PrimIsLower                           -> String
    "primIsLower"
        PrimitiveId
    PrimIsDigit                           -> String
    "primIsDigit"
        PrimitiveId
    PrimIsAlpha                           -> String
    "primIsAlpha"
        PrimitiveId
    PrimIsSpace                           -> String
    "primIsSpace"
        PrimitiveId
    PrimIsAscii                           -> String
    "primIsAscii"
        PrimitiveId
    PrimIsLatin1                          -> String
    "primIsLatin1"
        PrimitiveId
    PrimIsPrint                           -> String
    "primIsPrint"
        PrimitiveId
    PrimIsHexDigit                        -> String
    "primIsHexDigit"
        PrimitiveId
    PrimToUpper                           -> String
    "primToUpper"
        PrimitiveId
    PrimToLower                           -> String
    "primToLower"
        PrimitiveId
    PrimCharToNat                         -> String
    "primCharToNat"
        PrimitiveId
    PrimCharToNatInjective                -> String
    "primCharToNatInjective"
        PrimitiveId
    PrimNatToChar                         -> String
    "primNatToChar"
        PrimitiveId
    PrimShowChar                          -> String
    "primShowChar"
        -- String
        PrimitiveId
    PrimStringToList                      -> String
    "primStringToList"
        PrimitiveId
    PrimStringToListInjective             -> String
    "primStringToListInjective"
        PrimitiveId
    PrimStringFromList                    -> String
    "primStringFromList"
        PrimitiveId
    PrimStringFromListInjective           -> String
    "primStringFromListInjective"
        PrimitiveId
    PrimStringAppend                      -> String
    "primStringAppend"
        PrimitiveId
    PrimStringEquality                    -> String
    "primStringEquality"
        PrimitiveId
    PrimShowString                        -> String
    "primShowString"
        PrimitiveId
    PrimStringUncons                      -> String
    "primStringUncons"
        -- "Other stuff"
        PrimitiveId
    PrimErase                             -> String
    "primErase"
        PrimitiveId
    PrimEraseEquality                     -> String
    "primEraseEquality"
        PrimitiveId
    PrimForce                             -> String
    "primForce"
        PrimitiveId
    PrimForceLemma                        -> String
    "primForceLemma"
        PrimitiveId
    PrimQNameEquality                     -> String
    "primQNameEquality"
        PrimitiveId
    PrimQNameLess                         -> String
    "primQNameLess"
        PrimitiveId
    PrimShowQName                         -> String
    "primShowQName"
        PrimitiveId
    PrimQNameFixity                       -> String
    "primQNameFixity"
        PrimitiveId
    PrimQNameToWord64s                    -> String
    "primQNameToWord64s"
        PrimitiveId
    PrimQNameToWord64sInjective           -> String
    "primQNameToWord64sInjective"
        PrimitiveId
    PrimMetaEquality                      -> String
    "primMetaEquality"
        PrimitiveId
    PrimMetaLess                          -> String
    "primMetaLess"
        PrimitiveId
    PrimShowMeta                          -> String
    "primShowMeta"
        PrimitiveId
    PrimMetaToNat                         -> String
    "primMetaToNat"
        PrimitiveId
    PrimMetaToNatInjective                -> String
    "primMetaToNatInjective"
        PrimitiveId
    PrimLockUniv                          -> String
    "primLockUniv"

    builtinSubOut,
      builtinIMin, builtinIMax, builtinINeg,
      builtinGlue, builtin_glue, builtin_unglue, builtin_glueU, builtin_unglueU,
      builtinFaceForall, builtinComp, builtinPOr,
      builtinTrans,  builtinHComp, builtinLockUniv
      :: PrimitiveId
    builtinIMin :: PrimitiveId
    builtinIMin                              = PrimitiveId
    PrimIMin
    builtinIMax :: PrimitiveId
    builtinIMax                              = PrimitiveId
    PrimIMax
    builtinINeg :: PrimitiveId
    builtinINeg                              = PrimitiveId
    PrimINeg
    builtinSubOut :: PrimitiveId
    builtinSubOut                            = PrimitiveId
    PrimSubOut
    builtinGlue :: PrimitiveId
    builtinGlue                              = PrimitiveId
    PrimGlue
    builtin_glue :: PrimitiveId
    builtin_glue                             = PrimitiveId
    Prim_glue
    builtin_unglue :: PrimitiveId
    builtin_unglue                           = PrimitiveId
    Prim_unglue
    builtin_glueU :: PrimitiveId
    builtin_glueU                            = PrimitiveId
    Prim_glueU
    builtin_unglueU :: PrimitiveId
    builtin_unglueU                          = PrimitiveId
    Prim_unglueU
    builtinFaceForall :: PrimitiveId
    builtinFaceForall                        = PrimitiveId
    PrimFaceForall
    builtinComp :: PrimitiveId
    builtinComp                              = PrimitiveId
    PrimComp
    builtinPOr :: PrimitiveId
    builtinPOr                               = PrimitiveId
    PrimPOr
    builtinTrans :: PrimitiveId
    builtinTrans                             = PrimitiveId
    PrimTrans
    builtinHComp :: PrimitiveId
    builtinHComp                             = PrimitiveId
    PrimHComp
    builtinLockUniv :: PrimitiveId
    builtinLockUniv                          = PrimitiveId
    PrimLockUniv

    -- | Lookup a primitive by its identifier.
    primitiveById :: String -> Maybe PrimitiveId
    primitiveById :: String -> Maybe PrimitiveId
    primitiveById = (String -> Map String PrimitiveId -> Maybe PrimitiveId)
    -> Map String PrimitiveId -> String -> Maybe PrimitiveId
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip String -> Map String PrimitiveId -> Maybe PrimitiveId
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Map String PrimitiveId
    m where
      m :: Map String PrimitiveId
    m = [(String, PrimitiveId)] -> Map String PrimitiveId
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList [(PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    x, PrimitiveId
    x) | PrimitiveId
    x <- [(PrimitiveId
    forall a. Bounded a => a
    minBound :: PrimitiveId)..]]