type Rep SomeBuiltin = D1 ('MetaData "SomeBuiltin" "Agda.Syntax.Builtin" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "BuiltinName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 BuiltinId)) :+: C1 ('MetaCons "PrimitiveName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 PrimitiveId)))

type Rep BuiltinId = D1 ('MetaData "BuiltinId" "Agda.Syntax.Builtin" "Agda-2.6.20240714-inplace" 'False) (((((((C1 ('MetaCons "BuiltinNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinSuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinZero" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinNatPlus" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinNatMinus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinNatTimes" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinNatDivSucAux" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinNatModSucAux" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinNatEquals" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinNatLess" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinWord64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinInteger" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinIntegerPos" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinIntegerNegSuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinFloat" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinChar" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinString" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinUnit" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinUnitUnit" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinSigma" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSigmaCon" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinBool" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinTrue" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinFalse" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinList" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BuiltinNil" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinCons" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinMaybe" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinNothing" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinJust" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinIO" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinId" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinReflId" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinPath" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinPathP" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinIntervalUniv" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinInterval" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinIZero" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinIOne" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinPartial" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinPartialP" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinIsOne" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinItIsOne" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinEquiv" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinEquivFun" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinEquivProof" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinTranspProof" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinIsOne1" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinIsOne2" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinIsOneEmpty" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSub" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "BuiltinSubIn" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinSizeUniv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSize" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinSizeLt" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinSizeSuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSizeInf" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinSizeMax" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinInf" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSharp" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinFlat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinRefl" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinRewrite" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinLevelMax" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinLevel" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinLevelZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinLevelSuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinProp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinStrictSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinPropOmega" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinSetOmega" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinSSetOmega" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinLevelUniv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinFromNat" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BuiltinFromNeg" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinFromString" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinQName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaSort" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaSortSet" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaSortLit" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaSortProp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaSortPropLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaSortInf" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaSortUnsupported" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinHiding" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinHidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinInstance" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinVisible" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinRelevance" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinRelevant" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinIrrelevant" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinQuantity" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinQuantity0" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinQuantity\969" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinModality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinModalityConstructor" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAssoc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAssocLeft" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAssocRight" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAssocNon" 'PrefixI 'False) (U1 :: Type -> Type)))))))) :+: ((((((C1 ('MetaCons "BuiltinPrecedence" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinPrecRelated" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinPrecUnrelated" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinFixity" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinFixityFixity" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinArg" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinArgInfo" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinArgArgInfo" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinArgArg" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAbsAbs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTerm" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinAgdaTermVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTermLam" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTermExtLam" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTermDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTermCon" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTermPi" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaTermSort" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTermLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTermUnsupported" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaTermMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaErrorPart" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaErrorPartString" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaErrorPartTerm" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BuiltinAgdaErrorPartPatt" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaErrorPartName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaLiteral" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaLitNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaLitWord64" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaLitFloat" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaLitChar" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaLitString" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaLitQName" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaLitMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaClause" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaClauseClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaClauseAbsurd" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinAgdaPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaPatVar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaPatCon" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaPatDot" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaPatLit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaPatProj" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaPatAbsurd" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaDefinitionFunDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaDefinitionDataDef" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaDefinitionRecordDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaDefinitionDataConstructor" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaDefinitionPostulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaDefinitionPrimitive" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "BuiltinAgdaDefinition" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCM" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTCMReturn" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMBind" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMUnify" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMTypeError" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMInferType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMCheckType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTCMNormalise" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMReduce" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMCatchError" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinAgdaTCMGetContext" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMExtendContext" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMInContext" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTCMFreshName" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMDeclareDef" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMDeclarePostulate" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMDeclareData" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMDefineData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMDefineFun" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMGetType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMGetDefinition" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaTCMBlock" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMCommit" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "BuiltinAgdaTCMQuoteTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMUnquoteTerm" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMQuoteOmegaTerm" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTCMIsMacro" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMWithNormalisation" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMWithReconstructed" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMWithExpandLast" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMWithReduceDefs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMAskNormalisation" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMAskReconstructed" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMAskExpandLast" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaTCMAskReduceDefs" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMFormatErrorParts" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "BuiltinAgdaTCMDebugPrint" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMNoConstraints" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMWorkOnTypes" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "BuiltinAgdaTCMRunSpeculative" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMExec" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMGetInstances" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "BuiltinAgdaTCMSolveInstances" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BuiltinAgdaTCMPragmaForeign" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaTCMPragmaCompile" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "BuiltinAgdaBlocker" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaBlockerAny" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BuiltinAgdaBlockerAll" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BuiltinAgdaBlockerMeta" 'PrefixI 'False) (U1 :: Type -> Type)))))))))

type Rep PrimitiveId = D1 ('MetaData "PrimitiveId" "Agda.Syntax.Builtin" "Agda-2.6.20240714-inplace" 'False) ((((((C1 ('MetaCons "PrimConId" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimIdElim" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIMin" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimIMax" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimINeg" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimPartial" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimPartialP" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PrimSubOut" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimGlue" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Prim_glue" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "Prim_unglue" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Prim_glueU" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "Prim_unglueU" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFaceForall" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrimComp" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimPOr" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimTrans" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimDepIMin" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIdFace" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimIdPath" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimHComp" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "PrimShowInteger" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimNatPlus" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimNatMinus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimNatTimes" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimNatDivSucAux" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimNatModSucAux" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimNatEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimNatLess" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "PrimShowNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimWord64FromNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimWord64ToNat" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimWord64ToNatInjective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimLevelZero" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimLevelSuc" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimLevelMax" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PrimFloatEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimFloatInequality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatLess" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimFloatIsInfinite" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatIsNaN" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatIsNegativeZero" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatIsSafeInteger" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrimFloatToWord64" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimFloatToWord64Injective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimNatToFloat" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimIntToFloat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatRound" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatFloor" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatCeiling" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "PrimFloatToRatio" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimRatioToFloat" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatDecode" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatEncode" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimShowFloat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatPlus" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatMinus" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatTimes" 'PrefixI 'False) (U1 :: Type -> Type))))))) :+: (((((C1 ('MetaCons "PrimFloatNegate" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimFloatDiv" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatPow" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimFloatSqrt" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatExp" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatLog" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatSin" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PrimFloatCos" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimFloatTan" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatASin" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimFloatACos" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatATan" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimFloatATan2" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatSinh" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrimFloatCosh" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimFloatTanh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatASinh" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimFloatACosh" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimFloatATanh" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimCharEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIsLower" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "PrimIsDigit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIsAlpha" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimIsSpace" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIsAscii" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimIsLatin1" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimIsPrint" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimIsHexDigit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimToUpper" 'PrefixI 'False) (U1 :: Type -> Type)))))) :+: ((((C1 ('MetaCons "PrimToLower" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimCharToNat" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimCharToNatInjective" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimNatToChar" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimShowChar" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimStringToList" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimStringToListInjective" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "PrimStringFromList" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimStringFromListInjective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimStringAppend" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimStringEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimShowString" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimStringUncons" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimErase" 'PrefixI 'False) (U1 :: Type -> Type))))) :+: (((C1 ('MetaCons "PrimEraseEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimForce" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimForceLemma" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimQNameEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimQNameLess" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimShowQName" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimQNameFixity" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "PrimQNameToWord64s" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimQNameToWord64sInjective" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimMetaEquality" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimMetaLess" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "PrimShowMeta" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimMetaToNat" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PrimMetaToNatInjective" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "PrimLockUniv" 'PrefixI 'False) (U1 :: Type -> Type))))))))