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

Safe Haskell | None

Agda.TypeChecking.Monad.Builtin

Contents

- The names of built-in things

Synopsis

- litType :: Literal -> TCM Type
- getBuiltinThing :: String -> TCM (Maybe (Builtin PrimFun))
- setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
- bindBuiltinName :: String -> Term -> TCM ()
- bindPrimitive :: String -> PrimFun -> TCM ()
- getBuiltin :: String -> TCM Term
- getBuiltin' :: String -> TCM (Maybe Term)
- getPrimitive :: String -> TCM PrimFun
- primInteger :: TCM Term
- primAgdaRecordDef :: TCM Term
- primAgdaDataDef :: TCM Term
- primAgdaFunDef :: TCM Term
- primAgdaDefinitionDataConstructor :: TCM Term
- primAgdaDefinitionPrimitive :: TCM Term
- primAgdaDefinitionPostulate :: TCM Term
- primAgdaDefinitionRecordDef :: TCM Term
- primAgdaDefinitionDataDef :: TCM Term
- primAgdaDefinitionFunDef :: TCM Term
- primAgdaDefinition :: TCM Term
- primAgdaSortUnsupported :: TCM Term
- primAgdaSortLit :: TCM Term
- primAgdaSortSet :: TCM Term
- primAgdaSort :: TCM Term
- primIrrelevant :: TCM Term
- primRelevant :: TCM Term
- primRelevance :: TCM Term
- primVisible :: TCM Term
- primInstance :: TCM Term
- primHidden :: TCM Term
- primHiding :: TCM Term
- primAgdaTypeEl :: TCM Term
- primAgdaType :: TCM Term
- primAgdaTermUnsupported :: TCM Term
- primAgdaTermSort :: TCM Term
- primAgdaTermPi :: TCM Term
- primAgdaTermCon :: TCM Term
- primAgdaTermDef :: TCM Term
- primAgdaTermLam :: TCM Term
- primAgdaTermVar :: TCM Term
- primAgdaTerm :: TCM Term
- primArgArg :: TCM Term
- primArg :: TCM Term
- primQName :: TCM Term
- primIrrAxiom :: TCM Term
- primLevelMax :: TCM Term
- primLevelSuc :: TCM Term
- primLevelZero :: TCM Term
- primLevel :: TCM Term
- primRefl :: TCM Term
- primEquality :: TCM Term
- primFlat :: TCM Term
- primSharp :: TCM Term
- primInf :: TCM Term
- primSizeInf :: TCM Term
- primSizeSuc :: TCM Term
- primSizeLt :: TCM Term
- primSize :: TCM Term
- primNatLess :: TCM Term
- primNatEquality :: TCM Term
- primNatModSucAux :: TCM Term
- primNatDivSucAux :: TCM Term
- primNatTimes :: TCM Term
- primNatMinus :: TCM Term
- primNatPlus :: TCM Term
- primZero :: TCM Term
- primSuc :: TCM Term
- primNat :: TCM Term
- primIO :: TCM Term
- primCons :: TCM Term
- primNil :: TCM Term
- primList :: TCM Term
- primFalse :: TCM Term
- primTrue :: TCM Term
- primBool :: TCM Term
- primString :: TCM Term
- primChar :: TCM Term
- primFloat :: TCM Term
- primSizeMax :: TCM Term
- builtinNat :: [Char]
- builtinSuc :: [Char]
- builtinZero :: [Char]
- builtinNatPlus :: [Char]
- builtinNatMinus :: [Char]
- builtinNatTimes :: [Char]
- builtinNatDivSucAux :: [Char]
- builtinNatModSucAux :: [Char]
- builtinNatEquals :: [Char]
- builtinNatLess :: [Char]
- builtinInteger :: [Char]
- builtinFloat :: [Char]
- builtinChar :: [Char]
- builtinString :: [Char]
- builtinBool :: [Char]
- builtinTrue :: [Char]
- builtinFalse :: [Char]
- builtinList :: [Char]
- builtinNil :: [Char]
- builtinCons :: [Char]
- builtinIO :: [Char]
- builtinSize :: [Char]
- builtinSizeLt :: [Char]
- builtinSizeSuc :: [Char]
- builtinSizeInf :: [Char]
- builtinSizeMax :: [Char]
- builtinInf :: [Char]
- builtinSharp :: [Char]
- builtinFlat :: [Char]
- builtinEquality :: [Char]
- builtinRefl :: [Char]
- builtinLevelMax :: [Char]
- builtinLevel :: [Char]
- builtinLevelZero :: [Char]
- builtinLevelSuc :: [Char]
- builtinIrrAxiom :: [Char]
- builtinQName :: [Char]
- builtinAgdaSort :: [Char]
- builtinAgdaSortSet :: [Char]
- builtinAgdaSortLit :: [Char]
- builtinAgdaSortUnsupported :: [Char]
- builtinAgdaType :: [Char]
- builtinAgdaTypeEl :: [Char]
- builtinHiding :: [Char]
- builtinHidden :: [Char]
- builtinInstance :: [Char]
- builtinVisible :: [Char]
- builtinRelevance :: [Char]
- builtinRelevant :: [Char]
- builtinIrrelevant :: [Char]
- builtinArg :: [Char]
- builtinArgArg :: [Char]
- builtinAgdaTerm :: [Char]
- builtinAgdaTermVar :: [Char]
- builtinAgdaTermLam :: [Char]
- builtinAgdaTermDef :: [Char]
- builtinAgdaTermCon :: [Char]
- builtinAgdaTermPi :: [Char]
- builtinAgdaTermSort :: [Char]
- builtinAgdaTermUnsupported :: [Char]
- builtinAgdaFunDef :: [Char]
- builtinAgdaDataDef :: [Char]
- builtinAgdaRecordDef :: [Char]
- builtinAgdaDefinitionFunDef :: [Char]
- builtinAgdaDefinitionDataDef :: [Char]
- builtinAgdaDefinitionRecordDef :: [Char]
- builtinAgdaDefinitionDataConstructor :: [Char]
- builtinAgdaDefinitionPostulate :: [Char]
- builtinAgdaDefinitionPrimitive :: [Char]
- builtinAgdaDefinition :: [Char]
- data CoinductionKit = CoinductionKit {
  - nameOfInf :: QName
  - nameOfSharp :: QName
  - nameOfFlat :: QName
  }
- coinductionKit :: TCM (Maybe CoinductionKit)

# Documentation

litType :: Literal -> TCM Type

getBuiltinThing :: String -> TCM (Maybe (Builtin PrimFun))

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()

bindBuiltinName :: String -> Term -> TCM ()

bindPrimitive :: String -> PrimFun -> TCM ()

getBuiltin :: String -> TCM Term

getBuiltin' :: String -> TCM (Maybe Term)

getPrimitive :: String -> TCM PrimFun

# The names of built-in things

primInteger :: TCM Term

primAgdaRecordDef :: TCM Term

primAgdaDataDef :: TCM Term

primAgdaFunDef :: TCM Term

primAgdaDefinitionDataConstructor :: TCM Term

primAgdaDefinitionPrimitive :: TCM Term

primAgdaDefinitionPostulate :: TCM Term

primAgdaDefinitionRecordDef :: TCM Term

primAgdaDefinitionDataDef :: TCM Term

primAgdaDefinitionFunDef :: TCM Term

primAgdaDefinition :: TCM Term

primAgdaSortUnsupported :: TCM Term

primAgdaSortLit :: TCM Term

primAgdaSortSet :: TCM Term

primAgdaSort :: TCM Term

primIrrelevant :: TCM Term

primRelevant :: TCM Term

primRelevance :: TCM Term

primVisible :: TCM Term

primInstance :: TCM Term

primHidden :: TCM Term

primHiding :: TCM Term

primAgdaTypeEl :: TCM Term

primAgdaType :: TCM Term

primAgdaTermUnsupported :: TCM Term

primAgdaTermSort :: TCM Term

primAgdaTermPi :: TCM Term

primAgdaTermCon :: TCM Term

primAgdaTermDef :: TCM Term

primAgdaTermLam :: TCM Term

primAgdaTermVar :: TCM Term

primAgdaTerm :: TCM Term

primArgArg :: TCM Term

primArg :: TCM Term

primQName :: TCM Term

primIrrAxiom :: TCM Term

primLevelMax :: TCM Term

primLevelSuc :: TCM Term

primLevelZero :: TCM Term

primLevel :: TCM Term

primRefl :: TCM Term

primEquality :: TCM Term

primFlat :: TCM Term

primSharp :: TCM Term

primInf :: TCM Term

primSizeInf :: TCM Term

primSizeSuc :: TCM Term

primSizeLt :: TCM Term

primSize :: TCM Term

primNatLess :: TCM Term

primNatEquality :: TCM Term

primNatModSucAux :: TCM Term

primNatDivSucAux :: TCM Term

primNatTimes :: TCM Term

primNatMinus :: TCM Term

primNatPlus :: TCM Term

primZero :: TCM Term

primSuc :: TCM Term

primNat :: TCM Term

primIO :: TCM Term

primCons :: TCM Term

primNil :: TCM Term

primList :: TCM Term

primFalse :: TCM Term

primTrue :: TCM Term

primBool :: TCM Term

primString :: TCM Term

primChar :: TCM Term

primFloat :: TCM Term

primSizeMax :: TCM Term

builtinNat :: [Char]

builtinSuc :: [Char]

builtinZero :: [Char]

builtinNatPlus :: [Char]

builtinNatMinus :: [Char]

builtinNatTimes :: [Char]

builtinNatDivSucAux :: [Char]

builtinNatModSucAux :: [Char]

builtinNatEquals :: [Char]

builtinNatLess :: [Char]

builtinInteger :: [Char]

builtinFloat :: [Char]

builtinChar :: [Char]

builtinString :: [Char]

builtinBool :: [Char]

builtinTrue :: [Char]

builtinFalse :: [Char]

builtinList :: [Char]

builtinNil :: [Char]

builtinCons :: [Char]

builtinIO :: [Char]

builtinSize :: [Char]

builtinSizeLt :: [Char]

builtinSizeSuc :: [Char]

builtinSizeInf :: [Char]

builtinSizeMax :: [Char]

builtinInf :: [Char]

builtinSharp :: [Char]

builtinFlat :: [Char]

builtinEquality :: [Char]

builtinRefl :: [Char]

builtinLevelMax :: [Char]

builtinLevel :: [Char]

builtinLevelZero :: [Char]

builtinLevelSuc :: [Char]

builtinIrrAxiom :: [Char]

builtinQName :: [Char]

builtinAgdaSort :: [Char]

builtinAgdaSortSet :: [Char]

builtinAgdaSortLit :: [Char]

builtinAgdaSortUnsupported :: [Char]

builtinAgdaType :: [Char]

builtinAgdaTypeEl :: [Char]

builtinHiding :: [Char]

builtinHidden :: [Char]

builtinInstance :: [Char]

builtinVisible :: [Char]

builtinRelevance :: [Char]

builtinRelevant :: [Char]

builtinIrrelevant :: [Char]

builtinArg :: [Char]

builtinArgArg :: [Char]

builtinAgdaTerm :: [Char]

builtinAgdaTermVar :: [Char]

builtinAgdaTermLam :: [Char]

builtinAgdaTermDef :: [Char]

builtinAgdaTermCon :: [Char]

builtinAgdaTermPi :: [Char]

builtinAgdaTermSort :: [Char]

builtinAgdaTermUnsupported :: [Char]

builtinAgdaFunDef :: [Char]

builtinAgdaDataDef :: [Char]

builtinAgdaRecordDef :: [Char]

builtinAgdaDefinitionFunDef :: [Char]

builtinAgdaDefinitionDataDef :: [Char]

builtinAgdaDefinitionRecordDef :: [Char]

builtinAgdaDefinitionDataConstructor :: [Char]

builtinAgdaDefinitionPostulate :: [Char]

builtinAgdaDefinitionPrimitive :: [Char]

builtinAgdaDefinition :: [Char]

data CoinductionKit

The coinductive primitives.

Constructors

CoinductionKit |

Fields

nameOfInf :: QName
nameOfSharp :: QName
nameOfFlat :: QName

coinductionKit :: TCM (Maybe CoinductionKit)

Tries to build a `CoinductionKit`.