Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Builtin

Description

This module defines the names of all BUILTINs.

Synopsis

builtinNat :: String
builtinSuc :: String
builtinZero :: String
builtinNatPlus :: String
builtinNatMinus :: String
builtinNatTimes :: String
builtinNatDivSucAux :: String
builtinNatModSucAux :: String
builtinNatEquals :: String
builtinNatLess :: String
builtinInteger :: String
builtinIntegerPos :: String
builtinIntegerNegSuc :: String
builtinWord64 :: String
builtinFloat :: String
builtinChar :: String
builtinString :: String
builtinUnit :: String
builtinUnitUnit :: String
builtinSigma :: String
builtinBool :: String
builtinTrue :: String
builtinFalse :: String
builtinList :: String
builtinNil :: String
builtinCons :: String
builtinIO :: String
builtinMaybe :: String
builtinNothing :: String
builtinJust :: String
builtinPath :: String
builtinPathP :: String
builtinInterval :: String
builtinIZero :: String
builtinIOne :: String
builtinPartial :: String
builtinPartialP :: String
builtinIMin :: String
builtinIMax :: String
builtinINeg :: String
builtinIsOne :: String
builtinItIsOne :: String
builtinIsOne1 :: String
builtinIsOne2 :: String
builtinIsOneEmpty :: String
builtinComp :: String
builtinPOr :: String
builtinTrans :: String
builtinHComp :: String
builtinSub :: String
builtinSubIn :: String
builtinSubOut :: String
builtinEquiv :: String
builtinEquivFun :: String
builtinEquivProof :: String
builtinTranspProof :: String
builtinGlue :: String
builtin_glue :: String
builtin_unglue :: String
builtin_glueU :: String
builtin_unglueU :: String
builtinFaceForall :: String
builtinId :: String
builtinConId :: String
builtinIdElim :: String
builtinSizeUniv :: String
builtinSize :: String
builtinSizeLt :: String
builtinSizeSuc :: String
builtinSizeInf :: String
builtinSizeMax :: String
builtinInf :: String
builtinSharp :: String
builtinFlat :: String
builtinEquality :: String
builtinRefl :: String
builtinRewrite :: String
builtinLevelMax :: String
builtinLevel :: String
builtinLevelZero :: String
builtinLevelSuc :: String
builtinSet :: String
builtinProp :: String
builtinSetOmega :: String
builtinStrictSet :: String
builtinSSetOmega :: String
builtinLockUniv :: String
builtinFromNat :: String
builtinFromNeg :: String
builtinFromString :: String
builtinQName :: String
builtinAgdaSort :: String
builtinAgdaSortSet :: String
builtinAgdaSortLit :: String
builtinAgdaSortProp :: String
builtinAgdaSortPropLit :: String
builtinAgdaSortInf :: String
builtinAgdaSortUnsupported :: String
builtinHiding :: String
builtinHidden :: String
builtinInstance :: String
builtinVisible :: String
builtinRelevance :: String
builtinRelevant :: String
builtinIrrelevant :: String
builtinQuantity :: String
builtinQuantity0 :: String
builtinQuantityω :: String
builtinModality :: String
builtinModalityConstructor :: String
builtinAssoc :: String
builtinAssocLeft :: String
builtinAssocRight :: String
builtinAssocNon :: String
builtinPrecedence :: String
builtinPrecRelated :: String
builtinPrecUnrelated :: String
builtinFixity :: String
builtinFixityFixity :: String
builtinArgInfo :: String
builtinArgArgInfo :: String
builtinArg :: String
builtinArgArg :: String
builtinAbs :: String
builtinAbsAbs :: String
builtinAgdaTerm :: String
builtinAgdaTermVar :: String
builtinAgdaTermLam :: String
builtinAgdaTermExtLam :: String
builtinAgdaTermDef :: String
builtinAgdaTermCon :: String
builtinAgdaTermPi :: String
builtinAgdaTermSort :: String
builtinAgdaTermLit :: String
builtinAgdaTermUnsupported :: String
builtinAgdaTermMeta :: String
builtinAgdaErrorPart :: String
builtinAgdaErrorPartString :: String
builtinAgdaErrorPartTerm :: String
builtinAgdaErrorPartName :: String
builtinAgdaLiteral :: String
builtinAgdaLitNat :: String
builtinAgdaLitWord64 :: String
builtinAgdaLitFloat :: String
builtinAgdaLitChar :: String
builtinAgdaLitString :: String
builtinAgdaLitQName :: String
builtinAgdaLitMeta :: String
builtinAgdaClause :: String
builtinAgdaClauseClause :: String
builtinAgdaClauseAbsurd :: String
builtinAgdaPattern :: String
builtinAgdaPatVar :: String
builtinAgdaPatCon :: String
builtinAgdaPatDot :: String
builtinAgdaPatLit :: String
builtinAgdaPatProj :: String
builtinAgdaPatAbsurd :: String
builtinAgdaDefinitionFunDef :: String
builtinAgdaDefinitionDataDef :: String
builtinAgdaDefinitionRecordDef :: String
builtinAgdaDefinitionDataConstructor :: String
builtinAgdaDefinitionPostulate :: String
builtinAgdaDefinitionPrimitive :: String
builtinAgdaDefinition :: String
builtinAgdaMeta :: String
builtinAgdaTCM :: String
builtinAgdaTCMReturn :: String
builtinAgdaTCMBind :: String
builtinAgdaTCMUnify :: String
builtinAgdaTCMTypeError :: String
builtinAgdaTCMInferType :: String
builtinAgdaTCMCheckType :: String
builtinAgdaTCMNormalise :: String
builtinAgdaTCMReduce :: String
builtinAgdaTCMCatchError :: String
builtinAgdaTCMGetContext :: String
builtinAgdaTCMExtendContext :: String
builtinAgdaTCMInContext :: String
builtinAgdaTCMFreshName :: String
builtinAgdaTCMDeclareDef :: String
builtinAgdaTCMDeclarePostulate :: String
builtinAgdaTCMDefineFun :: String
builtinAgdaTCMGetType :: String
builtinAgdaTCMGetDefinition :: String
builtinAgdaTCMQuoteTerm :: String
builtinAgdaTCMUnquoteTerm :: String
builtinAgdaTCMQuoteOmegaTerm :: String
builtinAgdaTCMBlockOnMeta :: String
builtinAgdaTCMCommit :: String
builtinAgdaTCMIsMacro :: String
builtinAgdaTCMWithNormalisation :: String
builtinAgdaTCMWithReconsParams :: String
builtinAgdaTCMDebugPrint :: String
builtinAgdaTCMOnlyReduceDefs :: String
builtinAgdaTCMDontReduceDefs :: String
builtinAgdaTCMNoConstraints :: String
builtinAgdaTCMRunSpeculative :: String
builtinAgdaTCMExec :: String
isBuiltinNoDef :: String -> Bool
builtinsNoDef :: [String]
sizeBuiltins :: [String]

Documentation

builtinNat :: String Source #

builtinSuc :: String Source #

builtinZero :: String Source #

builtinNatPlus :: String Source #

builtinNatMinus :: String Source #

builtinNatTimes :: String Source #

builtinNatDivSucAux :: String Source #

builtinNatModSucAux :: String Source #

builtinNatEquals :: String Source #

builtinNatLess :: String Source #

builtinInteger :: String Source #

builtinIntegerPos :: String Source #

builtinIntegerNegSuc :: String Source #

builtinWord64 :: String Source #

builtinFloat :: String Source #

builtinChar :: String Source #

builtinString :: String Source #

builtinUnit :: String Source #

builtinUnitUnit :: String Source #

builtinSigma :: String Source #

builtinBool :: String Source #

builtinTrue :: String Source #

builtinFalse :: String Source #

builtinList :: String Source #

builtinNil :: String Source #

builtinCons :: String Source #

builtinIO :: String Source #

builtinMaybe :: String Source #

builtinNothing :: String Source #

builtinJust :: String Source #

builtinPath :: String Source #

builtinPathP :: String Source #

builtinInterval :: String Source #

builtinIZero :: String Source #

builtinIOne :: String Source #

builtinPartial :: String Source #

builtinPartialP :: String Source #

builtinIMin :: String Source #

builtinIMax :: String Source #

builtinINeg :: String Source #

builtinIsOne :: String Source #

builtinItIsOne :: String Source #

builtinIsOne1 :: String Source #

builtinIsOne2 :: String Source #

builtinIsOneEmpty :: String Source #

builtinComp :: String Source #

builtinPOr :: String Source #

builtinTrans :: String Source #

builtinHComp :: String Source #

builtinSub :: String Source #

builtinSubIn :: String Source #

builtinSubOut :: String Source #

builtinEquiv :: String Source #

builtinEquivFun :: String Source #

builtinEquivProof :: String Source #

builtinTranspProof :: String Source #

builtinGlue :: String Source #

builtin_glue :: String Source #

builtin_unglue :: String Source #

builtin_glueU :: String Source #

builtin_unglueU :: String Source #

builtinFaceForall :: String Source #

builtinId :: String Source #

builtinConId :: String Source #

builtinIdElim :: String Source #

builtinSizeUniv :: String Source #

builtinSize :: String Source #

builtinSizeLt :: String Source #

builtinSizeSuc :: String Source #

builtinSizeInf :: String Source #

builtinSizeMax :: String Source #

builtinInf :: String Source #

builtinSharp :: String Source #

builtinFlat :: String Source #

builtinEquality :: String Source #

builtinRefl :: String Source #

builtinRewrite :: String Source #

builtinLevelMax :: String Source #

builtinLevel :: String Source #

builtinLevelZero :: String Source #

builtinLevelSuc :: String Source #

builtinSet :: String Source #

builtinProp :: String Source #

builtinSetOmega :: String Source #

builtinStrictSet :: String Source #

builtinSSetOmega :: String Source #

builtinLockUniv :: String Source #

builtinFromNat :: String Source #

builtinFromNeg :: String Source #

builtinFromString :: String Source #

builtinQName :: String Source #

builtinAgdaSort :: String Source #

builtinAgdaSortSet :: String Source #

builtinAgdaSortLit :: String Source #

builtinAgdaSortProp :: String Source #

builtinAgdaSortPropLit :: String Source #

builtinAgdaSortInf :: String Source #

builtinAgdaSortUnsupported :: String Source #

builtinHiding :: String Source #

builtinHidden :: String Source #

builtinInstance :: String Source #

builtinVisible :: String Source #

builtinRelevance :: String Source #

builtinRelevant :: String Source #

builtinIrrelevant :: String Source #

builtinQuantity :: String Source #

builtinQuantity0 :: String Source #

builtinQuantityω :: String Source #

builtinModality :: String Source #

builtinModalityConstructor :: String Source #

builtinAssoc :: String Source #

builtinAssocLeft :: String Source #

builtinAssocRight :: String Source #

builtinAssocNon :: String Source #

builtinPrecedence :: String Source #

builtinPrecRelated :: String Source #

builtinPrecUnrelated :: String Source #

builtinFixity :: String Source #

builtinFixityFixity :: String Source #

builtinArgInfo :: String Source #

builtinArgArgInfo :: String Source #

builtinArg :: String Source #

builtinArgArg :: String Source #

builtinAbs :: String Source #

builtinAbsAbs :: String Source #

builtinAgdaTerm :: String Source #

builtinAgdaTermVar :: String Source #

builtinAgdaTermLam :: String Source #

builtinAgdaTermExtLam :: String Source #

builtinAgdaTermDef :: String Source #

builtinAgdaTermCon :: String Source #

builtinAgdaTermPi :: String Source #

builtinAgdaTermSort :: String Source #

builtinAgdaTermLit :: String Source #

builtinAgdaTermUnsupported :: String Source #

builtinAgdaTermMeta :: String Source #

builtinAgdaErrorPart :: String Source #

builtinAgdaErrorPartString :: String Source #

builtinAgdaErrorPartTerm :: String Source #

builtinAgdaErrorPartName :: String Source #

builtinAgdaLiteral :: String Source #

builtinAgdaLitNat :: String Source #

builtinAgdaLitWord64 :: String Source #

builtinAgdaLitFloat :: String Source #

builtinAgdaLitChar :: String Source #

builtinAgdaLitString :: String Source #

builtinAgdaLitQName :: String Source #

builtinAgdaLitMeta :: String Source #

builtinAgdaClause :: String Source #

builtinAgdaClauseClause :: String Source #

builtinAgdaClauseAbsurd :: String Source #

builtinAgdaPattern :: String Source #

builtinAgdaPatVar :: String Source #

builtinAgdaPatCon :: String Source #

builtinAgdaPatDot :: String Source #

builtinAgdaPatLit :: String Source #

builtinAgdaPatProj :: String Source #

builtinAgdaPatAbsurd :: String Source #

builtinAgdaDefinitionFunDef :: String Source #

builtinAgdaDefinitionDataDef :: String Source #

builtinAgdaDefinitionRecordDef :: String Source #

builtinAgdaDefinitionDataConstructor :: String Source #

builtinAgdaDefinitionPostulate :: String Source #

builtinAgdaDefinitionPrimitive :: String Source #

builtinAgdaDefinition :: String Source #

builtinAgdaMeta :: String Source #

builtinAgdaTCM :: String Source #

builtinAgdaTCMReturn :: String Source #

builtinAgdaTCMBind :: String Source #

builtinAgdaTCMUnify :: String Source #

builtinAgdaTCMTypeError :: String Source #

builtinAgdaTCMInferType :: String Source #

builtinAgdaTCMCheckType :: String Source #

builtinAgdaTCMNormalise :: String Source #

builtinAgdaTCMReduce :: String Source #

builtinAgdaTCMCatchError :: String Source #

builtinAgdaTCMGetContext :: String Source #

builtinAgdaTCMExtendContext :: String Source #

builtinAgdaTCMInContext :: String Source #

builtinAgdaTCMFreshName :: String Source #

builtinAgdaTCMDeclareDef :: String Source #

builtinAgdaTCMDeclarePostulate :: String Source #

builtinAgdaTCMDefineFun :: String Source #

builtinAgdaTCMGetType :: String Source #

builtinAgdaTCMGetDefinition :: String Source #

builtinAgdaTCMQuoteTerm :: String Source #

builtinAgdaTCMUnquoteTerm :: String Source #

builtinAgdaTCMQuoteOmegaTerm :: String Source #

builtinAgdaTCMBlockOnMeta :: String Source #

builtinAgdaTCMCommit :: String Source #

builtinAgdaTCMIsMacro :: String Source #

builtinAgdaTCMWithNormalisation :: String Source #

builtinAgdaTCMWithReconsParams :: String Source #

builtinAgdaTCMDebugPrint :: String Source #

builtinAgdaTCMOnlyReduceDefs :: String Source #

builtinAgdaTCMDontReduceDefs :: String Source #

builtinAgdaTCMNoConstraints :: String Source #

builtinAgdaTCMRunSpeculative :: String Source #

builtinAgdaTCMExec :: String Source #

isBuiltinNoDef :: String -> 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.

{--}

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

builtinsNoDef :: [String] Source #

sizeBuiltins :: [String] Source #