Agda.Syntax.Builtin

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

See Agda.TypeChecking.Monad.Builtin

Documentation

data SomeBuiltin

Either a BuiltinId or PrimitiveId, used for some lookups.

Constructors

BuiltinName !BuiltinId

PrimitiveName !PrimitiveId

Instances

IsBuiltin SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: SomeBuiltin -> SomeBuiltin

getBuiltinId :: SomeBuiltin -> String

EmbPrj SomeBuiltin

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: SomeBuiltin -> S Int32

icod_ :: SomeBuiltin -> S Int32

value :: Int32 -> R SomeBuiltin

Generic SomeBuiltin

Defined in Agda.Syntax.Builtin

Associated Types

type Rep SomeBuiltin :: Type -> Type

Methods

from :: SomeBuiltin -> Rep SomeBuiltin x

to :: Rep SomeBuiltin x -> SomeBuiltin

Show SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> SomeBuiltin -> ShowS

show :: SomeBuiltin -> String

showList :: [SomeBuiltin] -> ShowS

NFData SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

rnf :: SomeBuiltin -> ()

Eq SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

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

(/=) :: SomeBuiltin -> SomeBuiltin -> Bool

Ord SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

compare :: SomeBuiltin -> SomeBuiltin -> Ordering

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

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

(>) :: SomeBuiltin -> SomeBuiltin -> Bool

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

max :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin

min :: SomeBuiltin -> SomeBuiltin -> SomeBuiltin

Hashable SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> SomeBuiltin -> Int

hash :: SomeBuiltin -> Int

type Rep SomeBuiltin

Defined in Agda.Syntax.Builtin

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

class IsBuiltin a where

The class of types which can be converted to SomeBuiltin.

Methods

someBuiltin :: a -> SomeBuiltin

Convert this value to a builtin.

getBuiltinId :: a -> String

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

Instances

IsBuiltin BuiltinId

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: BuiltinId -> SomeBuiltin

getBuiltinId :: BuiltinId -> String

IsBuiltin PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: PrimitiveId -> SomeBuiltin

getBuiltinId :: PrimitiveId -> String

IsBuiltin SomeBuiltin

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: SomeBuiltin -> SomeBuiltin

getBuiltinId :: SomeBuiltin -> String

Builtins

data BuiltinId

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

BuiltinId

BuiltinReflId

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

BuiltinAgdaTCMRunSpeculative

BuiltinAgdaTCMExec

BuiltinAgdaTCMGetInstances

BuiltinAgdaTCMPragmaForeign

BuiltinAgdaTCMPragmaCompile

BuiltinAgdaBlocker

BuiltinAgdaBlockerAny

BuiltinAgdaBlockerAll

BuiltinAgdaBlockerMeta

Instances

IsBuiltin BuiltinId

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: BuiltinId -> SomeBuiltin

getBuiltinId :: BuiltinId -> String

Pretty BuiltinId

Defined in Agda.Syntax.Builtin

Methods

pretty :: BuiltinId -> Doc

prettyPrec :: Int -> BuiltinId -> Doc

prettyList :: [BuiltinId] -> Doc

KillRange BuiltinId

Defined in Agda.Syntax.Builtin

Methods

killRange :: KillRangeT BuiltinId

EmbPrj BuiltinId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: BuiltinId -> S Int32

icod_ :: BuiltinId -> S Int32

value :: Int32 -> R BuiltinId

Bounded BuiltinId

Defined in Agda.Syntax.Builtin

Methods

minBound :: BuiltinId

maxBound :: BuiltinId

Enum BuiltinId

Defined in Agda.Syntax.Builtin

Methods

succ :: BuiltinId -> BuiltinId

pred :: BuiltinId -> BuiltinId

toEnum :: Int -> BuiltinId

fromEnum :: BuiltinId -> Int

enumFrom :: BuiltinId -> [BuiltinId]

enumFromThen :: BuiltinId -> BuiltinId -> [BuiltinId]

enumFromTo :: BuiltinId -> BuiltinId -> [BuiltinId]

enumFromThenTo :: BuiltinId -> BuiltinId -> BuiltinId -> [BuiltinId]

Generic BuiltinId

Defined in Agda.Syntax.Builtin

Associated Types

type Rep BuiltinId :: Type -> Type

Methods

from :: BuiltinId -> Rep BuiltinId x

to :: Rep BuiltinId x -> BuiltinId

Show BuiltinId

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> BuiltinId -> ShowS

show :: BuiltinId -> String

showList :: [BuiltinId] -> ShowS

NFData BuiltinId

Defined in Agda.Syntax.Builtin

Methods

rnf :: BuiltinId -> ()

Eq BuiltinId

Defined in Agda.Syntax.Builtin

Methods

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

(/=) :: BuiltinId -> BuiltinId -> Bool

Ord BuiltinId

Defined in Agda.Syntax.Builtin

Methods

compare :: BuiltinId -> BuiltinId -> Ordering

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

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

(>) :: BuiltinId -> BuiltinId -> Bool

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

max :: BuiltinId -> BuiltinId -> BuiltinId

min :: BuiltinId -> BuiltinId -> BuiltinId

Hashable BuiltinId

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> BuiltinId -> Int

hash :: BuiltinId -> Int

type Rep BuiltinId

Defined in Agda.Syntax.Builtin

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

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]

sizeBuiltins :: [BuiltinId]

builtinNat :: BuiltinId

builtinSuc :: BuiltinId

builtinZero :: BuiltinId

builtinNatPlus :: BuiltinId

builtinNatMinus :: BuiltinId

builtinNatTimes :: BuiltinId

builtinNatDivSucAux :: BuiltinId

builtinNatModSucAux :: BuiltinId

builtinNatEquals :: BuiltinId

builtinNatLess :: BuiltinId

builtinInteger :: BuiltinId

builtinIntegerPos :: BuiltinId

builtinIntegerNegSuc :: BuiltinId

builtinWord64 :: 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

builtinIO :: BuiltinId

builtinMaybe :: BuiltinId

builtinNothing :: BuiltinId

builtinJust :: BuiltinId

builtinPath :: BuiltinId

builtinPathP :: BuiltinId

builtinInterval :: BuiltinId

builtinIZero :: BuiltinId

builtinIOne :: BuiltinId

builtinPartial :: BuiltinId

builtinPartialP :: BuiltinId

builtinIsOne :: BuiltinId

builtinItIsOne :: BuiltinId

builtinIsOne1 :: BuiltinId

builtinIsOne2 :: BuiltinId

builtinIsOneEmpty :: BuiltinId

builtinSub :: BuiltinId

builtinSubIn :: BuiltinId

builtinEquiv :: BuiltinId

builtinEquivFun :: BuiltinId

builtinEquivProof :: BuiltinId

builtinTranspProof :: BuiltinId

builtinId :: BuiltinId

builtinReflId :: 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

builtinIntervalUniv :: 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

builtinArgInfo :: BuiltinId

builtinArgArgInfo :: BuiltinId

builtinArg :: 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

builtinAgdaTCMQuoteTerm :: BuiltinId

builtinAgdaTCMUnquoteTerm :: BuiltinId

builtinAgdaTCMQuoteOmegaTerm :: BuiltinId

builtinAgdaTCMCommit :: BuiltinId

builtinAgdaTCMIsMacro :: BuiltinId

builtinAgdaTCMBlock :: BuiltinId

builtinAgdaBlocker :: BuiltinId

builtinAgdaBlockerAll :: BuiltinId

builtinAgdaBlockerAny :: BuiltinId

builtinAgdaBlockerMeta :: BuiltinId

builtinAgdaTCMFormatErrorParts :: BuiltinId

builtinAgdaTCMDebugPrint :: BuiltinId

builtinAgdaTCMWithNormalisation :: BuiltinId

builtinAgdaTCMWithReconstructed :: BuiltinId

builtinAgdaTCMWithExpandLast :: BuiltinId

builtinAgdaTCMWithReduceDefs :: BuiltinId

builtinAgdaTCMAskNormalisation :: BuiltinId

builtinAgdaTCMAskReconstructed :: BuiltinId

builtinAgdaTCMAskExpandLast :: BuiltinId

builtinAgdaTCMAskReduceDefs :: BuiltinId

builtinAgdaTCMNoConstraints :: BuiltinId

builtinAgdaTCMRunSpeculative :: BuiltinId

builtinAgdaTCMExec :: BuiltinId

builtinAgdaTCMGetInstances :: BuiltinId

builtinAgdaTCMPragmaForeign :: BuiltinId

builtinAgdaTCMPragmaCompile :: BuiltinId

builtinById :: String -> Maybe BuiltinId

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

Primitives

data PrimitiveId

A primitive name, defined by the primitive block.

Constructors

PrimConId

PrimIdElim

PrimIMin

PrimIMax

PrimINeg

PrimPartial

PrimPartialP

PrimSubOut

PrimGlue

Prim_glue

Prim_unglue

Prim_glueU

Prim_unglueU

PrimFaceForall

PrimComp

PrimPOr

PrimTrans

PrimDepIMin

PrimIdFace

PrimIdPath

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

IsBuiltin PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

someBuiltin :: PrimitiveId -> SomeBuiltin

getBuiltinId :: PrimitiveId -> String

Pretty PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

pretty :: PrimitiveId -> Doc

prettyPrec :: Int -> PrimitiveId -> Doc

prettyList :: [PrimitiveId] -> Doc

KillRange PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

killRange :: KillRangeT PrimitiveId

InstantiateFull PrimitiveId

Defined in Agda.TypeChecking.Reduce

Methods

instantiateFull' :: PrimitiveId -> ReduceM PrimitiveId

EmbPrj PrimitiveId

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: PrimitiveId -> S Int32

icod_ :: PrimitiveId -> S Int32

value :: Int32 -> R PrimitiveId

Bounded PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

minBound :: PrimitiveId

maxBound :: PrimitiveId

Enum PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

succ :: PrimitiveId -> PrimitiveId

pred :: PrimitiveId -> PrimitiveId

toEnum :: Int -> PrimitiveId

fromEnum :: PrimitiveId -> Int

enumFrom :: PrimitiveId -> [PrimitiveId]

enumFromThen :: PrimitiveId -> PrimitiveId -> [PrimitiveId]

enumFromTo :: PrimitiveId -> PrimitiveId -> [PrimitiveId]

enumFromThenTo :: PrimitiveId -> PrimitiveId -> PrimitiveId -> [PrimitiveId]

Generic PrimitiveId

Defined in Agda.Syntax.Builtin

Associated Types

type Rep PrimitiveId :: Type -> Type

Methods

from :: PrimitiveId -> Rep PrimitiveId x

to :: Rep PrimitiveId x -> PrimitiveId

Show PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> PrimitiveId -> ShowS

show :: PrimitiveId -> String

showList :: [PrimitiveId] -> ShowS

NFData PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

rnf :: PrimitiveId -> ()

Eq PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

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

(/=) :: PrimitiveId -> PrimitiveId -> Bool

Ord PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

compare :: PrimitiveId -> PrimitiveId -> Ordering

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

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

(>) :: PrimitiveId -> PrimitiveId -> Bool

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

max :: PrimitiveId -> PrimitiveId -> PrimitiveId

min :: PrimitiveId -> PrimitiveId -> PrimitiveId

Hashable PrimitiveId

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> PrimitiveId -> Int

hash :: PrimitiveId -> Int

type Rep PrimitiveId

Defined in Agda.Syntax.Builtin

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

builtinConId :: PrimitiveId

builtinIdElim :: PrimitiveId

builtinSubOut :: PrimitiveId

builtinIMin :: PrimitiveId

builtinIMax :: PrimitiveId

builtinINeg :: PrimitiveId

builtinGlue :: PrimitiveId

builtin_glue :: PrimitiveId

builtin_unglue :: PrimitiveId

builtin_glueU :: PrimitiveId

builtin_unglueU :: PrimitiveId

builtinFaceForall :: PrimitiveId

builtinComp :: PrimitiveId

builtinPOr :: PrimitiveId

builtinTrans :: PrimitiveId

builtinDepIMin :: PrimitiveId

builtinIdFace :: PrimitiveId

builtinIdPath :: PrimitiveId

builtinHComp :: PrimitiveId

builtinLockUniv :: PrimitiveId

primitiveById :: String -> Maybe PrimitiveId

Lookup a primitive by its identifier.