Agda.TypeChecking.Monad.Builtin

Documentation

class (Functor m, Applicative m, Monad m) => HasBuiltins m where

Methods

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

Instances

MonadIO m => HasBuiltins (TCMT m)

litType :: Literal -> TCM Type

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()

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

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

getBuiltin :: String -> TCM Term

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)

getPrimitive :: String -> TCM PrimFun

constructorForm :: Term -> TCM Term

Rewrite a literal to constructor form if possible.

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term

The names of built-in things

primInteger :: TCM Term

primFloat :: TCM Term

primChar :: TCM Term

primString :: TCM Term

primBool :: TCM Term

primTrue :: TCM Term

primFalse :: TCM Term

primList :: TCM Term

primNil :: TCM Term

primCons :: TCM Term

primIO :: TCM Term

primNat :: TCM Term

primSuc :: TCM Term

primZero :: TCM Term

primNatPlus :: TCM Term

primNatMinus :: TCM Term

primNatTimes :: TCM Term

primNatDivSucAux :: TCM Term

primNatModSucAux :: TCM Term

primNatEquality :: TCM Term

primNatLess :: TCM Term

primSizeUniv :: TCM Term

primSize :: TCM Term

primSizeLt :: TCM Term

primSizeSuc :: TCM Term

primSizeInf :: TCM Term

primSizeMax :: TCM Term

primInf :: TCM Term

primSharp :: TCM Term

primFlat :: TCM Term

primEquality :: TCM Term

primRefl :: TCM Term

primRewrite :: TCM Term

primLevel :: TCM Term

primLevelZero :: TCM Term

primLevelSuc :: TCM Term

primLevelMax :: TCM Term

primIrrAxiom :: TCM Term

primQName :: TCM Term

primArgInfo :: TCM Term

primArgArgInfo :: TCM Term

primArg :: TCM Term

primArgArg :: TCM Term

primAgdaTerm :: TCM Term

primAgdaTermVar :: TCM Term

primAgdaTermLam :: TCM Term

primAgdaTermExtLam :: TCM Term

primAgdaTermDef :: TCM Term

primAgdaTermCon :: TCM Term

primAgdaTermPi :: TCM Term

primAgdaTermSort :: TCM Term

primAgdaTermLit :: TCM Term

primAgdaTermUnsupported :: TCM Term

primAgdaType :: TCM Term

primAgdaTypeEl :: TCM Term

primHiding :: TCM Term

primHidden :: TCM Term

primInstance :: TCM Term

primVisible :: TCM Term

primRelevance :: TCM Term

primRelevant :: TCM Term

primIrrelevant :: TCM Term

primAgdaLiteral :: TCM Term

primAgdaLitNat :: TCM Term

primAgdaLitFloat :: TCM Term

primAgdaLitString :: TCM Term

primAgdaLitChar :: TCM Term

primAgdaLitQName :: TCM Term

primAgdaSort :: TCM Term

primAgdaSortSet :: TCM Term

primAgdaSortLit :: TCM Term

primAgdaSortUnsupported :: TCM Term

primAgdaDefinition :: TCM Term

primAgdaDefinitionFunDef :: TCM Term

primAgdaDefinitionDataDef :: TCM Term

primAgdaDefinitionRecordDef :: TCM Term

primAgdaDefinitionPostulate :: TCM Term

primAgdaDefinitionPrimitive :: TCM Term

primAgdaDefinitionDataConstructor :: TCM Term

primAgdaFunDef :: TCM Term

primAgdaFunDefCon :: TCM Term

primAgdaClause :: TCM Term

primAgdaClauseClause :: TCM Term

primAgdaClauseAbsurd :: TCM Term

primAgdaPattern :: TCM Term

primAgdaPatCon :: TCM Term

primAgdaPatVar :: TCM Term

primAgdaPatDot :: TCM Term

primAgdaDataDef :: TCM Term

primAgdaRecordDef :: TCM Term

primAgdaPatLit :: TCM Term

primAgdaPatProj :: TCM Term

primAgdaPatAbsurd :: TCM Term

builtinNat :: String

builtinSuc :: String

builtinZero :: String

builtinNatPlus :: String

builtinNatMinus :: String

builtinNatTimes :: String

builtinNatDivSucAux :: String

builtinNatModSucAux :: String

builtinNatEquals :: String

builtinNatLess :: String

builtinInteger :: String

builtinFloat :: String

builtinChar :: String

builtinString :: String

builtinBool :: String

builtinTrue :: String

builtinFalse :: String

builtinList :: String

builtinNil :: String

builtinCons :: String

builtinIO :: 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

builtinIrrAxiom :: String

builtinQName :: String

builtinAgdaSort :: String

builtinAgdaSortSet :: String

builtinAgdaSortLit :: String

builtinAgdaSortUnsupported :: String

builtinAgdaType :: String

builtinAgdaTypeEl :: String

builtinHiding :: String

builtinHidden :: String

builtinInstance :: String

builtinVisible :: String

builtinRelevance :: String

builtinRelevant :: String

builtinIrrelevant :: String

builtinArg :: String

builtinArgInfo :: String

builtinArgArgInfo :: String

builtinArgArg :: String

builtinAgdaTerm :: String

builtinAgdaTermVar :: String

builtinAgdaTermLam :: String

builtinAgdaTermExtLam :: String

builtinAgdaTermDef :: String

builtinAgdaTermCon :: String

builtinAgdaTermPi :: String

builtinAgdaTermSort :: String

builtinAgdaTermLit :: String

builtinAgdaTermUnsupported :: String

builtinAgdaLiteral :: String

builtinAgdaLitNat :: String

builtinAgdaLitFloat :: String

builtinAgdaLitChar :: String

builtinAgdaLitString :: String

builtinAgdaLitQName :: String

builtinAgdaFunDef :: String

builtinAgdaFunDefCon :: String

builtinAgdaClause :: String

builtinAgdaClauseClause :: String

builtinAgdaClauseAbsurd :: String

builtinAgdaPattern :: String

builtinAgdaPatVar :: String

builtinAgdaPatCon :: String

builtinAgdaPatDot :: String

builtinAgdaPatLit :: String

builtinAgdaPatProj :: String

builtinAgdaPatAbsurd :: String

builtinAgdaDataDef :: String

builtinAgdaRecordDef :: String

builtinAgdaDefinitionFunDef :: String

builtinAgdaDefinitionDataDef :: String

builtinAgdaDefinitionRecordDef :: String

builtinAgdaDefinitionDataConstructor :: String

builtinAgdaDefinitionPostulate :: String

builtinAgdaDefinitionPrimitive :: String

builtinAgdaDefinition :: String

builtinsNoDef :: [String]

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.

data CoinductionKit

The coinductive primitives.

Constructors

CoinductionKit

Fields

nameOfInf :: QName

nameOfSharp :: QName

nameOfFlat :: QName

coinductionKit' :: TCM CoinductionKit

Tries to build a CoinductionKit.

coinductionKit :: TCM (Maybe CoinductionKit)

Builtin equality

primEqualityName :: TCM QName

Get the name of the equality type.