Agda-2.6.4: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Builtin

Description

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

See Agda.TypeChecking.Monad.Builtin

Synopsis

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 Int32 Source #

icod_ :: SomeBuiltin -> S Int32 Source #

value :: Int32 -> R SomeBuiltin Source #

Generic SomeBuiltin Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> SomeBuiltin -> ShowS

show :: SomeBuiltin -> String

showList :: [SomeBuiltin] -> ShowS

NFData SomeBuiltin Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

rnf :: SomeBuiltin -> ()

Eq SomeBuiltin Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

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

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

Ord SomeBuiltin Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> SomeBuiltin -> Int

hash :: SomeBuiltin -> Int

type Rep SomeBuiltin Source # 
Instance details

Defined in Agda.Syntax.Builtin

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

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 Int32 Source #

icod_ :: BuiltinId -> S Int32 Source #

value :: Int32 -> R BuiltinId Source #

Bounded BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

minBound :: BuiltinId

maxBound :: BuiltinId

Enum BuiltinId Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> BuiltinId -> ShowS

show :: BuiltinId -> String

showList :: [BuiltinId] -> ShowS

NFData BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

rnf :: BuiltinId -> ()

Eq BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

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

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

Ord BuiltinId Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> BuiltinId -> Int

hash :: BuiltinId -> Int

type Rep BuiltinId Source # 
Instance details

Defined in Agda.Syntax.Builtin

type Rep BuiltinId = D1 ('MetaData "BuiltinId" "Agda.Syntax.Builtin" "Agda-2.6.4-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 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 #

builtinInteger :: BuiltinId Source #

builtinIntegerPos :: BuiltinId Source #

builtinIntegerNegSuc :: BuiltinId Source #

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

builtinIO :: BuiltinId Source #

builtinMaybe :: BuiltinId Source #

builtinNothing :: BuiltinId Source #

builtinJust :: BuiltinId Source #

builtinPath :: BuiltinId Source #

builtinPathP :: BuiltinId Source #

builtinInterval :: BuiltinId Source #

builtinIZero :: BuiltinId Source #

builtinIOne :: BuiltinId Source #

builtinPartial :: BuiltinId Source #

builtinPartialP :: BuiltinId Source #

builtinIsOne :: BuiltinId Source #

builtinItIsOne :: BuiltinId Source #

builtinIsOne1 :: BuiltinId Source #

builtinIsOne2 :: BuiltinId Source #

builtinIsOneEmpty :: BuiltinId Source #

builtinSub :: BuiltinId Source #

builtinSubIn :: BuiltinId Source #

builtinEquiv :: BuiltinId Source #

builtinEquivFun :: BuiltinId Source #

builtinEquivProof :: BuiltinId Source #

builtinTranspProof :: BuiltinId Source #

builtinId :: BuiltinId Source #

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

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

builtinArgInfo :: BuiltinId Source #

builtinArgArgInfo :: BuiltinId Source #

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

builtinAgdaTCMQuoteTerm :: BuiltinId Source #

builtinAgdaTCMUnquoteTerm :: BuiltinId Source #

builtinAgdaTCMQuoteOmegaTerm :: BuiltinId Source #

builtinAgdaTCMCommit :: BuiltinId Source #

builtinAgdaTCMIsMacro :: BuiltinId Source #

builtinAgdaTCMBlock :: BuiltinId Source #

builtinAgdaBlocker :: BuiltinId Source #

builtinAgdaBlockerAll :: BuiltinId Source #

builtinAgdaBlockerAny :: BuiltinId Source #

builtinAgdaBlockerMeta :: BuiltinId Source #

builtinAgdaTCMFormatErrorParts :: BuiltinId Source #

builtinAgdaTCMDebugPrint :: 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 #

builtinAgdaTCMNoConstraints :: BuiltinId Source #

builtinAgdaTCMRunSpeculative :: BuiltinId Source #

builtinAgdaTCMExec :: BuiltinId Source #

builtinAgdaTCMGetInstances :: BuiltinId Source #

builtinAgdaTCMPragmaForeign :: BuiltinId Source #

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

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

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 Int32 Source #

icod_ :: PrimitiveId -> S Int32 Source #

value :: Int32 -> R PrimitiveId Source #

Bounded PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

minBound :: PrimitiveId

maxBound :: PrimitiveId

Enum PrimitiveId Source # 
Instance details

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 Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

showsPrec :: Int -> PrimitiveId -> ShowS

show :: PrimitiveId -> String

showList :: [PrimitiveId] -> ShowS

NFData PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

rnf :: PrimitiveId -> ()

Eq PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

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

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

Ord PrimitiveId Source # 
Instance details

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 Source # 
Instance details

Defined in Agda.Syntax.Builtin

Methods

hashWithSalt :: Int -> PrimitiveId -> Int

hash :: PrimitiveId -> Int

type Rep PrimitiveId Source # 
Instance details

Defined in Agda.Syntax.Builtin

type Rep PrimitiveId = D1 ('MetaData "PrimitiveId" "Agda.Syntax.Builtin" "Agda-2.6.4-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 Source #

builtinIdElim :: PrimitiveId Source #

builtinSubOut :: PrimitiveId Source #

builtinIMin :: PrimitiveId Source #

builtinIMax :: PrimitiveId Source #

builtinINeg :: 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 #

builtinDepIMin :: PrimitiveId Source #

builtinIdFace :: PrimitiveId Source #

builtinIdPath :: PrimitiveId Source #

builtinHComp :: PrimitiveId Source #

builtinLockUniv :: PrimitiveId Source #

primitiveById :: String -> Maybe PrimitiveId Source #

Lookup a primitive by its identifier.