Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Builtin

Contents

- Builtins
- Primitives

Description

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

See Agda.TypeChecking.Monad.Builtin

Synopsis

- data SomeBuiltin
  - = BuiltinName !BuiltinId
  - | PrimitiveName !PrimitiveId
- class IsBuiltin a where
  - someBuiltin :: a -> SomeBuiltin
  - getBuiltinId :: a -> String
- 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
- isBuiltinNoDef :: BuiltinId -> Bool
- builtinsNoDef :: [BuiltinId]
- sizeBuiltins :: [BuiltinId]
- builtinNat :: BuiltinId
- builtinSuc :: BuiltinId
- builtinZero :: BuiltinId
- builtinNatPlus :: BuiltinId
- builtinNatMinus :: BuiltinId
- builtinNatTimes :: BuiltinId
- builtinNatDivSucAux :: BuiltinId
- builtinNatModSucAux :: BuiltinId
- builtinNatEquals :: BuiltinId
- builtinNatLess :: BuiltinId
- builtinWord64 :: BuiltinId
- builtinInteger :: BuiltinId
- builtinIntegerPos :: BuiltinId
- builtinIntegerNegSuc :: BuiltinId
- builtinFloat :: BuiltinId
- builtinChar :: BuiltinId
- builtinString :: BuiltinId
- builtinUnit :: BuiltinId
- builtinUnitUnit :: BuiltinId
- builtinSigma :: BuiltinId
- builtinBool :: BuiltinId
- builtinTrue :: BuiltinId
- builtinFalse :: BuiltinId
- builtinList :: BuiltinId
- builtinNil :: BuiltinId
- builtinCons :: BuiltinId
- builtinMaybe :: BuiltinId
- builtinNothing :: BuiltinId
- builtinJust :: BuiltinId
- builtinIO :: BuiltinId
- builtinPath :: BuiltinId
- builtinPathP :: BuiltinId
- builtinIntervalUniv :: BuiltinId
- builtinInterval :: BuiltinId
- builtinIZero :: BuiltinId
- builtinIOne :: BuiltinId
- builtinPartial :: BuiltinId
- builtinPartialP :: BuiltinId
- builtinIsOne :: BuiltinId
- builtinItIsOne :: BuiltinId
- builtinEquiv :: BuiltinId
- builtinEquivFun :: BuiltinId
- builtinEquivProof :: BuiltinId
- builtinTranspProof :: BuiltinId
- builtinIsOne1 :: BuiltinId
- builtinIsOne2 :: BuiltinId
- builtinIsOneEmpty :: BuiltinId
- builtinSub :: BuiltinId
- builtinSubIn :: BuiltinId
- builtinSizeUniv :: BuiltinId
- builtinSize :: BuiltinId
- builtinSizeLt :: BuiltinId
- builtinSizeSuc :: BuiltinId
- builtinSizeInf :: BuiltinId
- builtinSizeMax :: BuiltinId
- builtinInf :: BuiltinId
- builtinSharp :: BuiltinId
- builtinFlat :: BuiltinId
- builtinEquality :: BuiltinId
- builtinRefl :: BuiltinId
- builtinRewrite :: BuiltinId
- builtinLevelMax :: BuiltinId
- builtinLevel :: BuiltinId
- builtinLevelZero :: BuiltinId
- builtinLevelSuc :: BuiltinId
- builtinProp :: BuiltinId
- builtinSet :: BuiltinId
- builtinStrictSet :: BuiltinId
- builtinPropOmega :: BuiltinId
- builtinSetOmega :: BuiltinId
- builtinSSetOmega :: BuiltinId
- builtinLevelUniv :: BuiltinId
- builtinFromNat :: BuiltinId
- builtinFromNeg :: BuiltinId
- builtinFromString :: BuiltinId
- builtinQName :: BuiltinId
- builtinAgdaSort :: BuiltinId
- builtinAgdaSortSet :: BuiltinId
- builtinAgdaSortLit :: BuiltinId
- builtinAgdaSortProp :: BuiltinId
- builtinAgdaSortPropLit :: BuiltinId
- builtinAgdaSortInf :: BuiltinId
- builtinAgdaSortUnsupported :: BuiltinId
- builtinHiding :: BuiltinId
- builtinHidden :: BuiltinId
- builtinInstance :: BuiltinId
- builtinVisible :: BuiltinId
- builtinRelevance :: BuiltinId
- builtinRelevant :: BuiltinId
- builtinIrrelevant :: BuiltinId
- builtinQuantity :: BuiltinId
- builtinQuantity0 :: BuiltinId
- builtinQuantityω :: BuiltinId
- builtinModality :: BuiltinId
- builtinModalityConstructor :: BuiltinId
- builtinAssoc :: BuiltinId
- builtinAssocLeft :: BuiltinId
- builtinAssocRight :: BuiltinId
- builtinAssocNon :: BuiltinId
- builtinPrecedence :: BuiltinId
- builtinPrecRelated :: BuiltinId
- builtinPrecUnrelated :: BuiltinId
- builtinFixity :: BuiltinId
- builtinFixityFixity :: BuiltinId
- builtinArg :: BuiltinId
- builtinArgInfo :: BuiltinId
- builtinArgArgInfo :: BuiltinId
- builtinArgArg :: BuiltinId
- builtinAbs :: BuiltinId
- builtinAbsAbs :: BuiltinId
- builtinAgdaTerm :: BuiltinId
- builtinAgdaTermVar :: BuiltinId
- builtinAgdaTermLam :: BuiltinId
- builtinAgdaTermExtLam :: BuiltinId
- builtinAgdaTermDef :: BuiltinId
- builtinAgdaTermCon :: BuiltinId
- builtinAgdaTermPi :: BuiltinId
- builtinAgdaTermSort :: BuiltinId
- builtinAgdaTermLit :: BuiltinId
- builtinAgdaTermUnsupported :: BuiltinId
- builtinAgdaTermMeta :: BuiltinId
- builtinAgdaErrorPart :: BuiltinId
- builtinAgdaErrorPartString :: BuiltinId
- builtinAgdaErrorPartTerm :: BuiltinId
- builtinAgdaErrorPartPatt :: BuiltinId
- builtinAgdaErrorPartName :: BuiltinId
- builtinAgdaLiteral :: BuiltinId
- builtinAgdaLitNat :: BuiltinId
- builtinAgdaLitWord64 :: BuiltinId
- builtinAgdaLitFloat :: BuiltinId
- builtinAgdaLitChar :: BuiltinId
- builtinAgdaLitString :: BuiltinId
- builtinAgdaLitQName :: BuiltinId
- builtinAgdaLitMeta :: BuiltinId
- builtinAgdaClause :: BuiltinId
- builtinAgdaClauseClause :: BuiltinId
- builtinAgdaClauseAbsurd :: BuiltinId
- builtinAgdaPattern :: BuiltinId
- builtinAgdaPatVar :: BuiltinId
- builtinAgdaPatCon :: BuiltinId
- builtinAgdaPatDot :: BuiltinId
- builtinAgdaPatLit :: BuiltinId
- builtinAgdaPatProj :: BuiltinId
- builtinAgdaPatAbsurd :: BuiltinId
- builtinAgdaDefinitionFunDef :: BuiltinId
- builtinAgdaDefinitionDataDef :: BuiltinId
- builtinAgdaDefinitionRecordDef :: BuiltinId
- builtinAgdaDefinitionDataConstructor :: BuiltinId
- builtinAgdaDefinitionPostulate :: BuiltinId
- builtinAgdaDefinitionPrimitive :: BuiltinId
- builtinAgdaDefinition :: BuiltinId
- builtinAgdaMeta :: BuiltinId
- builtinAgdaTCM :: BuiltinId
- builtinAgdaTCMReturn :: BuiltinId
- builtinAgdaTCMBind :: BuiltinId
- builtinAgdaTCMUnify :: BuiltinId
- builtinAgdaTCMTypeError :: BuiltinId
- builtinAgdaTCMInferType :: BuiltinId
- builtinAgdaTCMCheckType :: BuiltinId
- builtinAgdaTCMNormalise :: BuiltinId
- builtinAgdaTCMReduce :: BuiltinId
- builtinAgdaTCMCatchError :: BuiltinId
- builtinAgdaTCMGetContext :: BuiltinId
- builtinAgdaTCMExtendContext :: BuiltinId
- builtinAgdaTCMInContext :: BuiltinId
- builtinAgdaTCMFreshName :: BuiltinId
- builtinAgdaTCMDeclareDef :: BuiltinId
- builtinAgdaTCMDeclarePostulate :: BuiltinId
- builtinAgdaTCMDeclareData :: BuiltinId
- builtinAgdaTCMDefineData :: BuiltinId
- builtinAgdaTCMDefineFun :: BuiltinId
- builtinAgdaTCMGetType :: BuiltinId
- builtinAgdaTCMGetDefinition :: BuiltinId
- builtinAgdaTCMBlock :: BuiltinId
- builtinAgdaTCMCommit :: BuiltinId
- builtinAgdaTCMQuoteTerm :: BuiltinId
- builtinAgdaTCMUnquoteTerm :: BuiltinId
- builtinAgdaTCMQuoteOmegaTerm :: BuiltinId
- builtinAgdaTCMIsMacro :: BuiltinId
- builtinAgdaTCMWithNormalisation :: BuiltinId
- builtinAgdaTCMWithReconstructed :: BuiltinId
- builtinAgdaTCMWithExpandLast :: BuiltinId
- builtinAgdaTCMWithReduceDefs :: BuiltinId
- builtinAgdaTCMAskNormalisation :: BuiltinId
- builtinAgdaTCMAskReconstructed :: BuiltinId
- builtinAgdaTCMAskExpandLast :: BuiltinId
- builtinAgdaTCMAskReduceDefs :: BuiltinId
- builtinAgdaTCMFormatErrorParts :: BuiltinId
- builtinAgdaTCMDebugPrint :: BuiltinId
- builtinAgdaTCMNoConstraints :: BuiltinId
- builtinAgdaTCMWorkOnTypes :: BuiltinId
- builtinAgdaTCMRunSpeculative :: BuiltinId
- builtinAgdaTCMExec :: BuiltinId
- builtinAgdaTCMCheckFromString :: BuiltinId
- builtinAgdaTCMGetInstances :: BuiltinId
- builtinAgdaTCMSolveInstances :: BuiltinId
- builtinAgdaTCMPragmaForeign :: BuiltinId
- builtinAgdaTCMPragmaCompile :: BuiltinId
- builtinAgdaBlocker :: BuiltinId
- builtinAgdaBlockerAny :: BuiltinId
- builtinAgdaBlockerAll :: BuiltinId
- builtinAgdaBlockerMeta :: BuiltinId
- builtinById :: String -> Maybe BuiltinId
- data PrimitiveId
  - = PrimIMin
  - | PrimIMax
  - | PrimINeg
  - | PrimPartial
  - | PrimPartialP
  - | PrimSubOut
  - | PrimGlue
  - | Prim_glue
  - | Prim_unglue
  - | Prim_glueU
  - | Prim_unglueU
  - | PrimFaceForall
  - | PrimComp
  - | PrimPOr
  - | PrimTrans
  - | PrimHComp
  - | PrimShowInteger
  - | PrimNatPlus
  - | PrimNatMinus
  - | PrimNatTimes
  - | PrimNatDivSucAux
  - | PrimNatModSucAux
  - | PrimNatEquality
  - | PrimNatLess
  - | PrimShowNat
  - | PrimWord64FromNat
  - | PrimWord64ToNat
  - | PrimWord64ToNatInjective
  - | PrimLevelZero
  - | PrimLevelSuc
  - | PrimLevelMax
  - | 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
  - | PrimCharEquality
  - | PrimIsLower
  - | PrimIsDigit
  - | PrimIsAlpha
  - | PrimIsSpace
  - | PrimIsAscii
  - | PrimIsLatin1
  - | PrimIsPrint
  - | PrimIsHexDigit
  - | PrimToUpper
  - | PrimToLower
  - | PrimCharToNat
  - | PrimCharToNatInjective
  - | PrimNatToChar
  - | PrimShowChar
  - | PrimStringToList
  - | PrimStringToListInjective
  - | PrimStringFromList
  - | PrimStringFromListInjective
  - | PrimStringAppend
  - | PrimStringEquality
  - | PrimShowString
  - | PrimStringUncons
  - | PrimErase
  - | PrimEraseEquality
  - | PrimForce
  - | PrimForceLemma
  - | PrimQNameEquality
  - | PrimQNameLess
  - | PrimShowQName
  - | PrimQNameFixity
  - | PrimQNameToWord64s
  - | PrimQNameToWord64sInjective
  - | PrimMetaEquality
  - | PrimMetaLess
  - | PrimShowMeta
  - | PrimMetaToNat
  - | PrimMetaToNatInjective
  - | PrimLockUniv
- builtinIMin :: PrimitiveId
- builtinIMax :: PrimitiveId
- builtinINeg :: PrimitiveId
- builtinSubOut :: PrimitiveId
- builtinGlue :: PrimitiveId
- builtin_glue :: PrimitiveId
- builtin_unglue :: PrimitiveId
- builtin_glueU :: PrimitiveId
- builtin_unglueU :: PrimitiveId
- builtinFaceForall :: PrimitiveId
- builtinComp :: PrimitiveId
- builtinPOr :: PrimitiveId
- builtinTrans :: PrimitiveId
- builtinHComp :: PrimitiveId
- builtinLockUniv :: PrimitiveId
- primitiveById :: String -> Maybe PrimitiveId

# Documentation

data SomeBuiltin Source #

Either a `BuiltinId` or `PrimitiveId`, used for some lookups.

Constructors

BuiltinName !BuiltinId |
PrimitiveName !PrimitiveId |

#### Instances

Instances details

IsBuiltin SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: SomeBuiltin -> SomeBuiltin Source # getBuiltinId :: SomeBuiltin -> String Source #
EmbPrj SomeBuiltin Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: SomeBuiltin -> S Word32 Source # icod_ :: SomeBuiltin -> S Word32 Source # value :: Word32 -> R SomeBuiltin Source #
NFData SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods rnf :: SomeBuiltin -> () Source #
Generic SomeBuiltin Source # |

Instance details

Defined in Agda.Syntax.Builtin

Associated Types

type Rep SomeBuiltin |

Instance details

Defined in Agda.Syntax.Builtin

type Rep SomeBuiltin = D1 ('MetaData "SomeBuiltin" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

Methods

from :: SomeBuiltin -> Rep SomeBuiltin x Source #

to :: Rep SomeBuiltin x -> SomeBuiltin Source #

Show SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods showsPrec :: Int -> SomeBuiltin -> ShowS Source # show :: SomeBuiltin -> String Source # showList :: [SomeBuiltin] -> ShowS Source #
Eq SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods (==) :: SomeBuiltin -> SomeBuiltin -> Bool Source # (/=) :: SomeBuiltin -> SomeBuiltin -> Bool Source #
Ord SomeBuiltin Source # |

Instance details

Defined in Agda.Syntax.Builtin

Methods

compare :: SomeBuiltin -> SomeBuiltin -> Ordering Source #

(<) :: SomeBuiltin -> SomeBuiltin -> Bool Source #

(<=) :: SomeBuiltin -> SomeBuiltin -> Bool Source #

(>) :: SomeBuiltin -> SomeBuiltin -> Bool Source #

(>=) :: SomeBuiltin -> SomeBuiltin -> Bool Source #

max :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin Source #

min :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin Source #

Hashable SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods hashWithSalt :: Int -> SomeBuiltin -> Int Source # hash :: SomeBuiltin -> Int Source #
type Rep SomeBuiltin Source # |

Instance details

Defined in Agda.Syntax.Builtin

type Rep SomeBuiltin = D1 ('MetaData "SomeBuiltin" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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)))

class IsBuiltin a where Source #

The class of types which can be converted to `SomeBuiltin`.

Methods

someBuiltin :: a -> SomeBuiltin Source #

Convert this value to a builtin.

getBuiltinId :: a -> String Source #

Get the identifier for this builtin, generally used for error messages.

#### Instances

Instances details

IsBuiltin BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: BuiltinId -> SomeBuiltin Source # getBuiltinId :: BuiltinId -> String Source #
IsBuiltin PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: PrimitiveId -> SomeBuiltin Source # getBuiltinId :: PrimitiveId -> String Source #
IsBuiltin SomeBuiltin Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: SomeBuiltin -> SomeBuiltin Source # getBuiltinId :: SomeBuiltin -> String Source #

# Builtins

data BuiltinId Source #

A builtin name, defined by the `BUILTIN` pragma.

Constructors

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 |

#### Instances

Instances details

IsBuiltin BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: BuiltinId -> SomeBuiltin Source # getBuiltinId :: BuiltinId -> String Source #
Pretty BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods pretty :: BuiltinId -> Doc Source # prettyPrec :: Int -> BuiltinId -> Doc Source # prettyList :: [BuiltinId] -> Doc Source #
KillRange BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods killRange :: KillRangeT BuiltinId Source #
EmbPrj BuiltinId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: BuiltinId -> S Word32 Source # icod_ :: BuiltinId -> S Word32 Source # value :: Word32 -> R BuiltinId Source #
NFData BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods rnf :: BuiltinId -> () Source #
Bounded BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods minBound :: BuiltinId Source # maxBound :: BuiltinId Source #
Enum BuiltinId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Methods

succ :: BuiltinId -> BuiltinId Source #

pred :: BuiltinId -> BuiltinId Source #

toEnum :: Int -> BuiltinId Source #

fromEnum :: BuiltinId -> Int Source #

enumFrom :: BuiltinId -> [BuiltinId] Source #

enumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId] Source #

enumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId] Source #

enumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId] Source #

Generic BuiltinId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Associated Types

type Rep BuiltinId |

Instance details

Defined in Agda.Syntax.Builtin

type Rep BuiltinId = D1 ('MetaData "BuiltinId" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "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 "BuiltinAgdaTCMCheckFromString" '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)))))))))

Methods

from :: BuiltinId -> Rep BuiltinId x Source #

to :: Rep BuiltinId x -> BuiltinId Source #

Show BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods showsPrec :: Int -> BuiltinId -> ShowS Source # show :: BuiltinId -> String Source # showList :: [BuiltinId] -> ShowS Source #
Eq BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods (==) :: BuiltinId -> BuiltinId -> Bool Source # (/=) :: BuiltinId -> BuiltinId -> Bool Source #
Ord BuiltinId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Methods

compare :: BuiltinId -> BuiltinId -> Ordering Source #

(<) :: BuiltinId -> BuiltinId -> Bool Source #

(<=) :: BuiltinId -> BuiltinId -> Bool Source #

(>) :: BuiltinId -> BuiltinId -> Bool Source #

(>=) :: BuiltinId -> BuiltinId -> Bool Source #

max :: BuiltinId -> BuiltinId -> BuiltinId Source #

min :: BuiltinId -> BuiltinId -> BuiltinId Source #

Hashable BuiltinId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods hashWithSalt :: Int -> BuiltinId -> Int Source # hash :: BuiltinId -> Int Source #
type Rep BuiltinId Source # |

Instance details

Defined in Agda.Syntax.Builtin

type Rep BuiltinId = D1 ('MetaData "BuiltinId" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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 "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 "BuiltinAgdaTCMCheckFromString" '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)))))))))

isBuiltinNoDef :: BuiltinId -> Bool Source #

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

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

{-# BUILTIN TYPE Type #-}

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

builtinsNoDef :: [BuiltinId] Source #

sizeBuiltins :: [BuiltinId] Source #

builtinNat :: BuiltinId Source #

builtinSuc :: BuiltinId Source #

builtinZero :: BuiltinId Source #

builtinNatPlus :: BuiltinId Source #

builtinNatMinus :: BuiltinId Source #

builtinNatTimes :: BuiltinId Source #

builtinNatDivSucAux :: BuiltinId Source #

builtinNatModSucAux :: BuiltinId Source #

builtinNatEquals :: BuiltinId Source #

builtinNatLess :: BuiltinId Source #

builtinWord64 :: BuiltinId Source #

builtinInteger :: BuiltinId Source #

builtinIntegerPos :: BuiltinId Source #

builtinIntegerNegSuc :: BuiltinId Source #

builtinFloat :: BuiltinId Source #

builtinChar :: BuiltinId Source #

builtinString :: BuiltinId Source #

builtinUnit :: BuiltinId Source #

builtinUnitUnit :: BuiltinId Source #

builtinSigma :: BuiltinId Source #

builtinBool :: BuiltinId Source #

builtinTrue :: BuiltinId Source #

builtinFalse :: BuiltinId Source #

builtinList :: BuiltinId Source #

builtinNil :: BuiltinId Source #

builtinCons :: BuiltinId Source #

builtinMaybe :: BuiltinId Source #

builtinNothing :: BuiltinId Source #

builtinJust :: BuiltinId Source #

builtinIO :: BuiltinId Source #

builtinPath :: BuiltinId Source #

builtinPathP :: BuiltinId Source #

builtinIntervalUniv :: BuiltinId Source #

builtinInterval :: BuiltinId Source #

builtinIZero :: BuiltinId Source #

builtinIOne :: BuiltinId Source #

builtinPartial :: BuiltinId Source #

builtinPartialP :: BuiltinId Source #

builtinIsOne :: BuiltinId Source #

builtinItIsOne :: BuiltinId Source #

builtinEquiv :: BuiltinId Source #

builtinEquivFun :: BuiltinId Source #

builtinEquivProof :: BuiltinId Source #

builtinTranspProof :: BuiltinId Source #

builtinIsOne1 :: BuiltinId Source #

builtinIsOne2 :: BuiltinId Source #

builtinIsOneEmpty :: BuiltinId Source #

builtinSub :: BuiltinId Source #

builtinSubIn :: BuiltinId Source #

builtinSizeUniv :: BuiltinId Source #

builtinSize :: BuiltinId Source #

builtinSizeLt :: BuiltinId Source #

builtinSizeSuc :: BuiltinId Source #

builtinSizeInf :: BuiltinId Source #

builtinSizeMax :: BuiltinId Source #

builtinInf :: BuiltinId Source #

builtinSharp :: BuiltinId Source #

builtinFlat :: BuiltinId Source #

builtinEquality :: BuiltinId Source #

builtinRefl :: BuiltinId Source #

builtinRewrite :: BuiltinId Source #

builtinLevelMax :: BuiltinId Source #

builtinLevel :: BuiltinId Source #

builtinLevelZero :: BuiltinId Source #

builtinLevelSuc :: BuiltinId Source #

builtinProp :: BuiltinId Source #

builtinSet :: BuiltinId Source #

builtinStrictSet :: BuiltinId Source #

builtinPropOmega :: BuiltinId Source #

builtinSetOmega :: BuiltinId Source #

builtinSSetOmega :: BuiltinId Source #

builtinLevelUniv :: BuiltinId Source #

builtinFromNat :: BuiltinId Source #

builtinFromNeg :: BuiltinId Source #

builtinFromString :: BuiltinId Source #

builtinQName :: BuiltinId Source #

builtinAgdaSort :: BuiltinId Source #

builtinAgdaSortSet :: BuiltinId Source #

builtinAgdaSortLit :: BuiltinId Source #

builtinAgdaSortProp :: BuiltinId Source #

builtinAgdaSortPropLit :: BuiltinId Source #

builtinAgdaSortInf :: BuiltinId Source #

builtinAgdaSortUnsupported :: BuiltinId Source #

builtinHiding :: BuiltinId Source #

builtinHidden :: BuiltinId Source #

builtinInstance :: BuiltinId Source #

builtinVisible :: BuiltinId Source #

builtinRelevance :: BuiltinId Source #

builtinRelevant :: BuiltinId Source #

builtinIrrelevant :: BuiltinId Source #

builtinQuantity :: BuiltinId Source #

builtinQuantity0 :: BuiltinId Source #

builtinQuantityω :: BuiltinId Source #

builtinModality :: BuiltinId Source #

builtinModalityConstructor :: BuiltinId Source #

builtinAssoc :: BuiltinId Source #

builtinAssocLeft :: BuiltinId Source #

builtinAssocRight :: BuiltinId Source #

builtinAssocNon :: BuiltinId Source #

builtinPrecedence :: BuiltinId Source #

builtinPrecRelated :: BuiltinId Source #

builtinPrecUnrelated :: BuiltinId Source #

builtinFixity :: BuiltinId Source #

builtinFixityFixity :: BuiltinId Source #

builtinArg :: BuiltinId Source #

builtinArgInfo :: BuiltinId Source #

builtinArgArgInfo :: BuiltinId Source #

builtinArgArg :: BuiltinId Source #

builtinAbs :: BuiltinId Source #

builtinAbsAbs :: BuiltinId Source #

builtinAgdaTerm :: BuiltinId Source #

builtinAgdaTermVar :: BuiltinId Source #

builtinAgdaTermLam :: BuiltinId Source #

builtinAgdaTermExtLam :: BuiltinId Source #

builtinAgdaTermDef :: BuiltinId Source #

builtinAgdaTermCon :: BuiltinId Source #

builtinAgdaTermPi :: BuiltinId Source #

builtinAgdaTermSort :: BuiltinId Source #

builtinAgdaTermLit :: BuiltinId Source #

builtinAgdaTermUnsupported :: BuiltinId Source #

builtinAgdaTermMeta :: BuiltinId Source #

builtinAgdaErrorPart :: BuiltinId Source #

builtinAgdaErrorPartString :: BuiltinId Source #

builtinAgdaErrorPartTerm :: BuiltinId Source #

builtinAgdaErrorPartPatt :: BuiltinId Source #

builtinAgdaErrorPartName :: BuiltinId Source #

builtinAgdaLiteral :: BuiltinId Source #

builtinAgdaLitNat :: BuiltinId Source #

builtinAgdaLitWord64 :: BuiltinId Source #

builtinAgdaLitFloat :: BuiltinId Source #

builtinAgdaLitChar :: BuiltinId Source #

builtinAgdaLitString :: BuiltinId Source #

builtinAgdaLitQName :: BuiltinId Source #

builtinAgdaLitMeta :: BuiltinId Source #

builtinAgdaClause :: BuiltinId Source #

builtinAgdaClauseClause :: BuiltinId Source #

builtinAgdaClauseAbsurd :: BuiltinId Source #

builtinAgdaPattern :: BuiltinId Source #

builtinAgdaPatVar :: BuiltinId Source #

builtinAgdaPatCon :: BuiltinId Source #

builtinAgdaPatDot :: BuiltinId Source #

builtinAgdaPatLit :: BuiltinId Source #

builtinAgdaPatProj :: BuiltinId Source #

builtinAgdaPatAbsurd :: BuiltinId Source #

builtinAgdaDefinitionFunDef :: BuiltinId Source #

builtinAgdaDefinitionDataDef :: BuiltinId Source #

builtinAgdaDefinitionRecordDef :: BuiltinId Source #

builtinAgdaDefinitionDataConstructor :: BuiltinId Source #

builtinAgdaDefinitionPostulate :: BuiltinId Source #

builtinAgdaDefinitionPrimitive :: BuiltinId Source #

builtinAgdaDefinition :: BuiltinId Source #

builtinAgdaMeta :: BuiltinId Source #

builtinAgdaTCM :: BuiltinId Source #

builtinAgdaTCMReturn :: BuiltinId Source #

builtinAgdaTCMBind :: BuiltinId Source #

builtinAgdaTCMUnify :: BuiltinId Source #

builtinAgdaTCMTypeError :: BuiltinId Source #

builtinAgdaTCMInferType :: BuiltinId Source #

builtinAgdaTCMCheckType :: BuiltinId Source #

builtinAgdaTCMNormalise :: BuiltinId Source #

builtinAgdaTCMReduce :: BuiltinId Source #

builtinAgdaTCMCatchError :: BuiltinId Source #

builtinAgdaTCMGetContext :: BuiltinId Source #

builtinAgdaTCMExtendContext :: BuiltinId Source #

builtinAgdaTCMInContext :: BuiltinId Source #

builtinAgdaTCMFreshName :: BuiltinId Source #

builtinAgdaTCMDeclareDef :: BuiltinId Source #

builtinAgdaTCMDeclarePostulate :: BuiltinId Source #

builtinAgdaTCMDeclareData :: BuiltinId Source #

builtinAgdaTCMDefineData :: BuiltinId Source #

builtinAgdaTCMDefineFun :: BuiltinId Source #

builtinAgdaTCMGetType :: BuiltinId Source #

builtinAgdaTCMGetDefinition :: BuiltinId Source #

builtinAgdaTCMBlock :: BuiltinId Source #

builtinAgdaTCMCommit :: BuiltinId Source #

builtinAgdaTCMQuoteTerm :: BuiltinId Source #

builtinAgdaTCMUnquoteTerm :: BuiltinId Source #

builtinAgdaTCMQuoteOmegaTerm :: BuiltinId Source #

builtinAgdaTCMIsMacro :: BuiltinId Source #

builtinAgdaTCMWithNormalisation :: BuiltinId Source #

builtinAgdaTCMWithReconstructed :: BuiltinId Source #

builtinAgdaTCMWithExpandLast :: BuiltinId Source #

builtinAgdaTCMWithReduceDefs :: BuiltinId Source #

builtinAgdaTCMAskNormalisation :: BuiltinId Source #

builtinAgdaTCMAskReconstructed :: BuiltinId Source #

builtinAgdaTCMAskExpandLast :: BuiltinId Source #

builtinAgdaTCMAskReduceDefs :: BuiltinId Source #

builtinAgdaTCMFormatErrorParts :: BuiltinId Source #

builtinAgdaTCMDebugPrint :: BuiltinId Source #

builtinAgdaTCMNoConstraints :: BuiltinId Source #

builtinAgdaTCMWorkOnTypes :: BuiltinId Source #

builtinAgdaTCMRunSpeculative :: BuiltinId Source #

builtinAgdaTCMExec :: BuiltinId Source #

builtinAgdaTCMCheckFromString :: BuiltinId Source #

builtinAgdaTCMGetInstances :: BuiltinId Source #

builtinAgdaTCMSolveInstances :: BuiltinId Source #

builtinAgdaTCMPragmaForeign :: BuiltinId Source #

builtinAgdaTCMPragmaCompile :: BuiltinId Source #

builtinAgdaBlocker :: BuiltinId Source #

builtinAgdaBlockerAny :: BuiltinId Source #

builtinAgdaBlockerAll :: BuiltinId Source #

builtinAgdaBlockerMeta :: BuiltinId Source #

builtinById :: String -> Maybe BuiltinId Source #

Lookup a builtin by the string used in the `BUILTIN` pragma.

# Primitives

data PrimitiveId Source #

A primitive name, defined by the `primitive` block.

Constructors

PrimIMin |
PrimIMax |
PrimINeg |
PrimPartial |
PrimPartialP |
PrimSubOut |
PrimGlue |
Prim_glue |
Prim_unglue |
Prim_glueU |
Prim_unglueU |
PrimFaceForall |
PrimComp |
PrimPOr |
PrimTrans |
PrimHComp |
PrimShowInteger |
PrimNatPlus |
PrimNatMinus |
PrimNatTimes |
PrimNatDivSucAux |
PrimNatModSucAux |
PrimNatEquality |
PrimNatLess |
PrimShowNat |
PrimWord64FromNat |
PrimWord64ToNat |
PrimWord64ToNatInjective |
PrimLevelZero |
PrimLevelSuc |
PrimLevelMax |
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 |
PrimCharEquality |
PrimIsLower |
PrimIsDigit |
PrimIsAlpha |
PrimIsSpace |
PrimIsAscii |
PrimIsLatin1 |
PrimIsPrint |
PrimIsHexDigit |
PrimToUpper |
PrimToLower |
PrimCharToNat |
PrimCharToNatInjective |
PrimNatToChar |
PrimShowChar |
PrimStringToList |
PrimStringToListInjective |
PrimStringFromList |
PrimStringFromListInjective |
PrimStringAppend |
PrimStringEquality |
PrimShowString |
PrimStringUncons |
PrimErase |
PrimEraseEquality |
PrimForce |
PrimForceLemma |
PrimQNameEquality |
PrimQNameLess |
PrimShowQName |
PrimQNameFixity |
PrimQNameToWord64s |
PrimQNameToWord64sInjective |
PrimMetaEquality |
PrimMetaLess |
PrimShowMeta |
PrimMetaToNat |
PrimMetaToNatInjective |
PrimLockUniv |

#### Instances

Instances details

IsBuiltin PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods someBuiltin :: PrimitiveId -> SomeBuiltin Source # getBuiltinId :: PrimitiveId -> String Source #
Pretty PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods pretty :: PrimitiveId -> Doc Source # prettyPrec :: Int -> PrimitiveId -> Doc Source # prettyList :: [PrimitiveId] -> Doc Source #
KillRange PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods killRange :: KillRangeT PrimitiveId Source #
InstantiateFull PrimitiveId Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: PrimitiveId -> ReduceM PrimitiveId Source #
EmbPrj PrimitiveId Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: PrimitiveId -> S Word32 Source # icod_ :: PrimitiveId -> S Word32 Source # value :: Word32 -> R PrimitiveId Source #
NFData PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods rnf :: PrimitiveId -> () Source #
Bounded PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods minBound :: PrimitiveId Source # maxBound :: PrimitiveId Source #
Enum PrimitiveId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Methods

succ :: PrimitiveId -> PrimitiveId Source #

pred :: PrimitiveId -> PrimitiveId Source #

toEnum :: Int -> PrimitiveId Source #

fromEnum :: PrimitiveId -> Int Source #

enumFrom :: PrimitiveId -> [PrimitiveId] Source #

enumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId] Source #

enumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId] Source #

enumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId] Source #

Generic PrimitiveId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Associated Types

type Rep PrimitiveId |

Instance details

Defined in Agda.Syntax.Builtin

type Rep PrimitiveId = D1 ('MetaData "PrimitiveId" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((((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 "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))))))))

Methods

from :: PrimitiveId -> Rep PrimitiveId x Source #

to :: Rep PrimitiveId x -> PrimitiveId Source #

Show PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods showsPrec :: Int -> PrimitiveId -> ShowS Source # show :: PrimitiveId -> String Source # showList :: [PrimitiveId] -> ShowS Source #
Eq PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods (==) :: PrimitiveId -> PrimitiveId -> Bool Source # (/=) :: PrimitiveId -> PrimitiveId -> Bool Source #
Ord PrimitiveId Source # |

Instance details

Defined in Agda.Syntax.Builtin

Methods

compare :: PrimitiveId -> PrimitiveId -> Ordering Source #

(<) :: PrimitiveId -> PrimitiveId -> Bool Source #

(<=) :: PrimitiveId -> PrimitiveId -> Bool Source #

(>) :: PrimitiveId -> PrimitiveId -> Bool Source #

(>=) :: PrimitiveId -> PrimitiveId -> Bool Source #

max :: PrimitiveId -> PrimitiveId -> PrimitiveId Source #

min :: PrimitiveId -> PrimitiveId -> PrimitiveId Source #

Hashable PrimitiveId Source # |
Instance details Defined in Agda.Syntax.Builtin Methods hashWithSalt :: Int -> PrimitiveId -> Int Source # hash :: PrimitiveId -> Int Source #
type Rep PrimitiveId Source # |

Instance details

Defined in Agda.Syntax.Builtin

type Rep PrimitiveId = D1 ('MetaData "PrimitiveId" "Agda.Syntax.Builtin" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((((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 "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))))))))

builtinIMin :: PrimitiveId Source #

builtinIMax :: PrimitiveId Source #

builtinINeg :: PrimitiveId Source #

builtinSubOut :: PrimitiveId Source #

builtinGlue :: PrimitiveId Source #

builtin_glue :: PrimitiveId Source #

builtin_unglue :: PrimitiveId Source #

builtin_glueU :: PrimitiveId Source #

builtin_unglueU :: PrimitiveId Source #

builtinFaceForall :: PrimitiveId Source #

builtinComp :: PrimitiveId Source #

builtinPOr :: PrimitiveId Source #

builtinTrans :: PrimitiveId Source #

builtinHComp :: PrimitiveId Source #

builtinLockUniv :: PrimitiveId Source #

primitiveById :: String -> Maybe PrimitiveId Source #

Lookup a primitive by its identifier.