HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Builtin

This module defines the names of all builtin and primitives used in Agda.

See Agda.TypeChecking.Monad.Builtin

  • 3 types
  • 1 class
  • 228 values
  • PackageAgda-2.7.0.1
  • Exports232
  • LanguageHaskell2010
  • LicenceMIT
  • SourceBuiltin.hs
datadata SomeBuiltin
#

Either a BuiltinId or PrimitiveId, used for some lookups.

Constructors

Instances9Eq, Ord, Show, Generic, NFData, Hashable, …

Builtins

208 declarations
datadata BuiltinId
#

A builtin name, defined by the BUILTIN pragma.

BuiltinNatBuiltinSucBuiltinZeroBuiltinNatPlusBuiltinNatMinusBuiltinNatTimesBuiltinNatDivSucAuxBuiltinNatModSucAuxBuiltinNatEqualsBuiltinNatLessBuiltinWord64BuiltinIntegerBuiltinIntegerPosBuiltinIntegerNegSucBuiltinFloatBuiltinCharBuiltinStringBuiltinUnitBuiltinUnitUnitBuiltinSigmaBuiltinSigmaConBuiltinBoolBuiltinTrueBuiltinFalseBuiltinListBuiltinNilBuiltinConsBuiltinMaybeBuiltinNothingBuiltinJustBuiltinIOBuiltinIdBuiltinReflIdBuiltinPathBuiltinPathPBuiltinIntervalUnivBuiltinIntervalBuiltinIZeroBuiltinIOneBuiltinPartialBuiltinPartialPBuiltinIsOneBuiltinItIsOneBuiltinEquivBuiltinEquivFunBuiltinEquivProofBuiltinTranspProofBuiltinIsOne1BuiltinIsOne2BuiltinIsOneEmptyBuiltinSubBuiltinSubInBuiltinSizeUnivBuiltinSizeBuiltinSizeLtBuiltinSizeSucBuiltinSizeInfBuiltinSizeMaxBuiltinInfBuiltinSharpBuiltinFlatBuiltinEqualityBuiltinReflBuiltinRewriteBuiltinLevelMaxBuiltinLevelBuiltinLevelZeroBuiltinLevelSucBuiltinPropBuiltinSetBuiltinStrictSetBuiltinPropOmegaBuiltinSetOmegaBuiltinSSetOmegaBuiltinLevelUnivBuiltinFromNatBuiltinFromNegBuiltinFromStringBuiltinQNameBuiltinAgdaSortBuiltinAgdaSortSetBuiltinAgdaSortLitBuiltinAgdaSortPropBuiltinAgdaSortPropLitBuiltinAgdaSortInfBuiltinAgdaSortUnsupportedBuiltinHidingBuiltinHiddenBuiltinInstanceBuiltinVisibleBuiltinRelevanceBuiltinRelevantBuiltinIrrelevantBuiltinQuantityBuiltinQuantity0BuiltinQuantityωBuiltinModalityBuiltinModalityConstructorBuiltinAssocBuiltinAssocLeftBuiltinAssocRightBuiltinAssocNonBuiltinPrecedenceBuiltinPrecRelatedBuiltinPrecUnrelatedBuiltinFixityBuiltinFixityFixityBuiltinArgBuiltinArgInfoBuiltinArgArgInfoBuiltinArgArgBuiltinAbsBuiltinAbsAbsBuiltinAgdaTermBuiltinAgdaTermVarBuiltinAgdaTermLamBuiltinAgdaTermExtLamBuiltinAgdaTermDefBuiltinAgdaTermConBuiltinAgdaTermPiBuiltinAgdaTermSortBuiltinAgdaTermLitBuiltinAgdaTermUnsupportedBuiltinAgdaTermMetaBuiltinAgdaErrorPartBuiltinAgdaErrorPartStringBuiltinAgdaErrorPartTermBuiltinAgdaErrorPartPattBuiltinAgdaErrorPartNameBuiltinAgdaLiteralBuiltinAgdaLitNatBuiltinAgdaLitWord64BuiltinAgdaLitFloatBuiltinAgdaLitCharBuiltinAgdaLitStringBuiltinAgdaLitQNameBuiltinAgdaLitMetaBuiltinAgdaClauseBuiltinAgdaClauseClauseBuiltinAgdaClauseAbsurdBuiltinAgdaPatternBuiltinAgdaPatVarBuiltinAgdaPatConBuiltinAgdaPatDotBuiltinAgdaPatLitBuiltinAgdaPatProjBuiltinAgdaPatAbsurdBuiltinAgdaDefinitionFunDefBuiltinAgdaDefinitionDataDefBuiltinAgdaDefinitionRecordDefBuiltinAgdaDefinitionDataConstructorBuiltinAgdaDefinitionPostulateBuiltinAgdaDefinitionPrimitiveBuiltinAgdaDefinitionBuiltinAgdaMetaBuiltinAgdaTCMBuiltinAgdaTCMReturnBuiltinAgdaTCMBindBuiltinAgdaTCMUnifyBuiltinAgdaTCMTypeErrorBuiltinAgdaTCMInferTypeBuiltinAgdaTCMCheckTypeBuiltinAgdaTCMNormaliseBuiltinAgdaTCMReduceBuiltinAgdaTCMCatchErrorBuiltinAgdaTCMGetContextBuiltinAgdaTCMExtendContextBuiltinAgdaTCMInContextBuiltinAgdaTCMFreshNameBuiltinAgdaTCMDeclareDefBuiltinAgdaTCMDeclarePostulateBuiltinAgdaTCMDeclareDataBuiltinAgdaTCMDefineDataBuiltinAgdaTCMDefineFunBuiltinAgdaTCMGetTypeBuiltinAgdaTCMGetDefinitionBuiltinAgdaTCMBlockBuiltinAgdaTCMCommitBuiltinAgdaTCMQuoteTermBuiltinAgdaTCMUnquoteTermBuiltinAgdaTCMQuoteOmegaTermBuiltinAgdaTCMIsMacroBuiltinAgdaTCMWithNormalisationBuiltinAgdaTCMWithReconstructedBuiltinAgdaTCMWithExpandLastBuiltinAgdaTCMWithReduceDefsBuiltinAgdaTCMAskNormalisationBuiltinAgdaTCMAskReconstructedBuiltinAgdaTCMAskExpandLastBuiltinAgdaTCMAskReduceDefsBuiltinAgdaTCMFormatErrorPartsBuiltinAgdaTCMDebugPrintBuiltinAgdaTCMNoConstraintsBuiltinAgdaTCMWorkOnTypesBuiltinAgdaTCMRunSpeculativeBuiltinAgdaTCMExecBuiltinAgdaTCMGetInstancesBuiltinAgdaTCMSolveInstancesBuiltinAgdaTCMPragmaForeignBuiltinAgdaTCMPragmaCompileBuiltinAgdaBlockerBuiltinAgdaBlockerAnyBuiltinAgdaBlockerAllBuiltinAgdaBlockerMeta
Instances13Bounded, Enum, Eq, Ord, Show, Generic, …
valueisBuiltinNoDef :: BuiltinId -> Bool
#

Builtins that come without a definition in Agda syntax. These are giving names to Agda internal concepts which cannot be assigned an Agda type.

An example would be a user-defined name for Set.

{-# BUILTIN TYPE Type #-}

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

Primitives

22 declarations
datadata PrimitiveId
#

A primitive name, defined by the primitive block.

PrimConIdPrimIdElimPrimIMinPrimIMaxPrimINegPrimPartialPrimPartialPPrimSubOutPrimGluePrim_gluePrim_ungluePrim_glueUPrim_unglueUPrimFaceForallPrimCompPrimPOrPrimTransPrimDepIMinPrimIdFacePrimIdPathPrimHCompPrimShowIntegerPrimNatPlusPrimNatMinusPrimNatTimesPrimNatDivSucAuxPrimNatModSucAuxPrimNatEqualityPrimNatLessPrimShowNatPrimWord64FromNatPrimWord64ToNatPrimWord64ToNatInjectivePrimLevelZeroPrimLevelSucPrimLevelMaxPrimFloatEqualityPrimFloatInequalityPrimFloatLessPrimFloatIsInfinitePrimFloatIsNaNPrimFloatIsNegativeZeroPrimFloatIsSafeIntegerPrimFloatToWord64PrimFloatToWord64InjectivePrimNatToFloatPrimIntToFloatPrimFloatRoundPrimFloatFloorPrimFloatCeilingPrimFloatToRatioPrimRatioToFloatPrimFloatDecodePrimFloatEncodePrimShowFloatPrimFloatPlusPrimFloatMinusPrimFloatTimesPrimFloatNegatePrimFloatDivPrimFloatPowPrimFloatSqrtPrimFloatExpPrimFloatLogPrimFloatSinPrimFloatCosPrimFloatTanPrimFloatASinPrimFloatACosPrimFloatATanPrimFloatATan2PrimFloatSinhPrimFloatCoshPrimFloatTanhPrimFloatASinhPrimFloatACoshPrimFloatATanhPrimCharEqualityPrimIsLowerPrimIsDigitPrimIsAlphaPrimIsSpacePrimIsAsciiPrimIsLatin1PrimIsPrintPrimIsHexDigitPrimToUpperPrimToLowerPrimCharToNatPrimCharToNatInjectivePrimNatToCharPrimShowCharPrimStringToListPrimStringToListInjectivePrimStringFromListPrimStringFromListInjectivePrimStringAppendPrimStringEqualityPrimShowStringPrimStringUnconsPrimErasePrimEraseEqualityPrimForcePrimForceLemmaPrimQNameEqualityPrimQNameLessPrimShowQNamePrimQNameFixityPrimQNameToWord64sPrimQNameToWord64sInjectivePrimMetaEqualityPrimMetaLessPrimShowMetaPrimMetaToNatPrimMetaToNatInjectivePrimLockUniv
Instances14Bounded, Enum, Eq, Ord, Show, Generic, …