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

Safe Haskell | Safe
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
- 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
- builtinPathToEquiv :: String
- builtinGlue :: String
- builtin_glue :: String
- builtin_unglue :: 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
- builtinSetOmega :: String
- builtinFromNat :: String
- builtinFromNeg :: String
- builtinFromString :: String
- builtinQName :: String
- builtinAgdaSort :: String
- builtinAgdaSortSet :: String
- builtinAgdaSortLit :: String
- builtinAgdaSortUnsupported :: String
- builtinHiding :: String
- builtinHidden :: String
- builtinInstance :: String
- builtinVisible :: String
- builtinRelevance :: String
- builtinRelevant :: String
- builtinIrrelevant :: String
- builtinArg :: String
- builtinAssoc :: String
- builtinAssocLeft :: String
- builtinAssocRight :: String
- builtinAssocNon :: String
- builtinPrecedence :: String
- builtinPrecRelated :: String
- builtinPrecUnrelated :: String
- builtinFixity :: String
- builtinFixityFixity :: String
- builtinArgInfo :: String
- builtinArgArgInfo :: 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
- builtinAgdaTCMBlockOnMeta :: String
- builtinAgdaTCMCommit :: String
- builtinAgdaTCMIsMacro :: String
- builtinAgdaTCMWithNormalisation :: String
- builtinAgdaTCMDebugPrint :: String
- builtinAgdaTCMNoConstraints :: String
- builtinAgdaTCMRunSpeculative :: String
- 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 #

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 #

builtinPathToEquiv :: String Source #

builtinGlue :: String Source #

builtin_glue :: String Source #

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

builtinSetOmega :: String Source #

builtinFromNat :: String Source #

builtinFromNeg :: String Source #

builtinFromString :: String Source #

builtinQName :: String Source #

builtinAgdaSort :: String Source #

builtinAgdaSortSet :: String Source #

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

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

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 #

builtinAgdaTCMBlockOnMeta :: String Source #

builtinAgdaTCMCommit :: String Source #

builtinAgdaTCMIsMacro :: String Source #

builtinAgdaTCMWithNormalisation :: String Source #

builtinAgdaTCMDebugPrint :: String Source #

builtinAgdaTCMNoConstraints :: String Source #

builtinAgdaTCMRunSpeculative :: String Source #

builtinsNoDef :: [String] 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.

sizeBuiltins :: [String] Source #