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 #
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 #
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 #
sizeBuiltins :: [String] Source #