| Safe Haskell | Safe-Inferred |
|---|---|
| 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
- builtinReflId :: 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
- builtinIntervalUniv :: 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
- builtinAgdaErrorPartPatt :: 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
- builtinAgdaTCMDeclareData :: String
- builtinAgdaTCMDefineData :: String
- builtinAgdaTCMDefineFun :: String
- builtinAgdaTCMGetType :: String
- builtinAgdaTCMGetDefinition :: String
- builtinAgdaTCMQuoteTerm :: String
- builtinAgdaTCMUnquoteTerm :: String
- builtinAgdaTCMQuoteOmegaTerm :: String
- builtinAgdaTCMBlockOnMeta :: String
- builtinAgdaTCMCommit :: String
- builtinAgdaTCMIsMacro :: String
- builtinAgdaTCMFormatErrorParts :: String
- builtinAgdaTCMDebugPrint :: String
- builtinAgdaTCMWithNormalisation :: String
- builtinAgdaTCMWithReconsParams :: String
- builtinAgdaTCMOnlyReduceDefs :: String
- builtinAgdaTCMDontReduceDefs :: String
- builtinAgdaTCMNoConstraints :: String
- builtinAgdaTCMRunSpeculative :: String
- builtinAgdaTCMExec :: String
- builtinAgdaTCMGetInstances :: String
- isBuiltinNoDef :: String -> Bool
- builtinsNoDef :: [String]
- sizeBuiltins :: [String]
Documentation
builtinNat :: String Source #
builtinSuc :: String Source #
builtinZero :: String Source #
builtinChar :: String Source #
builtinUnit :: String Source #
builtinBool :: String Source #
builtinTrue :: String Source #
builtinList :: String Source #
builtinNil :: String Source #
builtinCons :: String Source #
builtinJust :: String Source #
builtinPath :: String Source #
builtinIOne :: String Source #
builtinIMin :: String Source #
builtinIMax :: String Source #
builtinINeg :: String Source #
builtinComp :: String Source #
builtinPOr :: String Source #
builtinSub :: String Source #
builtinGlue :: String Source #
builtinSize :: String Source #
builtinInf :: String Source #
builtinFlat :: String Source #
builtinRefl :: String Source #
builtinSet :: String Source #
builtinProp :: String Source #
builtinArg :: String Source #
builtinAbs :: 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.
{-# BUILTIN TYPE Type #-}
The type of Type would be Type : Level → Setω
which is not valid Agda.
builtinsNoDef :: [String] Source #
sizeBuiltins :: [String] Source #