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

Agda.TypeChecking.Monad.Builtin

Contents

- The names of built-in things

Synopsis

- getBuiltinThings :: MonadTCM tcm => tcm (BuiltinThings PrimFun)
- setBuiltinThings :: MonadTCM tcm => BuiltinThings PrimFun -> tcm ()
- bindBuiltinName :: MonadTCM tcm => String -> Term -> tcm ()
- bindPrimitive :: MonadTCM tcm => String -> PrimFun -> tcm ()
- getBuiltin :: MonadTCM tcm => String -> tcm Term
- getBuiltin' :: MonadTCM tcm => String -> tcm (Maybe Term)
- getPrimitive :: MonadTCM tcm => String -> tcm PrimFun
- primFloat :: MonadTCM tcm => tcm Term
- primChar :: MonadTCM tcm => tcm Term
- primString :: MonadTCM tcm => tcm Term
- primBool :: MonadTCM tcm => tcm Term
- primTrue :: MonadTCM tcm => tcm Term
- primFalse :: MonadTCM tcm => tcm Term
- primList :: MonadTCM tcm => tcm Term
- primNil :: MonadTCM tcm => tcm Term
- primCons :: MonadTCM tcm => tcm Term
- primIO :: MonadTCM tcm => tcm Term
- primNat :: MonadTCM tcm => tcm Term
- primSuc :: MonadTCM tcm => tcm Term
- primZero :: MonadTCM tcm => tcm Term
- primNatPlus :: MonadTCM tcm => tcm Term
- primNatMinus :: MonadTCM tcm => tcm Term
- primNatTimes :: MonadTCM tcm => tcm Term
- primNatDivSucAux :: MonadTCM tcm => tcm Term
- primNatModSucAux :: MonadTCM tcm => tcm Term
- primNatEquality :: MonadTCM tcm => tcm Term
- primNatLess :: MonadTCM tcm => tcm Term
- primSize :: MonadTCM tcm => tcm Term
- primSizeSuc :: MonadTCM tcm => tcm Term
- primSizeInf :: MonadTCM tcm => tcm Term
- primInf :: MonadTCM tcm => tcm Term
- primSharp :: MonadTCM tcm => tcm Term
- primFlat :: MonadTCM tcm => tcm Term
- primEquality :: MonadTCM tcm => tcm Term
- primRefl :: MonadTCM tcm => tcm Term
- primLevel :: MonadTCM tcm => tcm Term
- primLevelZero :: MonadTCM tcm => tcm Term
- primLevelSuc :: MonadTCM tcm => tcm Term
- primLevelMax :: MonadTCM tcm => tcm Term
- primQName :: MonadTCM tcm => tcm Term
- primArg :: MonadTCM tcm => tcm Term
- primArgArg :: MonadTCM tcm => tcm Term
- primAgdaTerm :: MonadTCM tcm => tcm Term
- primAgdaTermVar :: MonadTCM tcm => tcm Term
- primAgdaTermLam :: MonadTCM tcm => tcm Term
- primAgdaTermDef :: MonadTCM tcm => tcm Term
- primAgdaTermCon :: MonadTCM tcm => tcm Term
- primAgdaTermPi :: MonadTCM tcm => tcm Term
- primAgdaTermSort :: MonadTCM tcm => tcm Term
- primAgdaTermUnsupported :: MonadTCM tcm => tcm Term
- primInteger :: MonadTCM tcm => tcm Term
- builtinTypes :: [String]

# Documentation

getBuiltinThings :: MonadTCM tcm => tcm (BuiltinThings PrimFun)

setBuiltinThings :: MonadTCM tcm => BuiltinThings PrimFun -> tcm ()

bindBuiltinName :: MonadTCM tcm => String -> Term -> tcm ()

bindPrimitive :: MonadTCM tcm => String -> PrimFun -> tcm ()

getBuiltin :: MonadTCM tcm => String -> tcm Term

getBuiltin' :: MonadTCM tcm => String -> tcm (Maybe Term)

getPrimitive :: MonadTCM tcm => String -> tcm PrimFun

# The names of built-in things

primFloat :: MonadTCM tcm => tcm Term

primChar :: MonadTCM tcm => tcm Term

primString :: MonadTCM tcm => tcm Term

primBool :: MonadTCM tcm => tcm Term

primTrue :: MonadTCM tcm => tcm Term

primFalse :: MonadTCM tcm => tcm Term

primList :: MonadTCM tcm => tcm Term

primNil :: MonadTCM tcm => tcm Term

primCons :: MonadTCM tcm => tcm Term

primIO :: MonadTCM tcm => tcm Term

primNat :: MonadTCM tcm => tcm Term

primSuc :: MonadTCM tcm => tcm Term

primZero :: MonadTCM tcm => tcm Term

primNatPlus :: MonadTCM tcm => tcm Term

primNatMinus :: MonadTCM tcm => tcm Term

primNatTimes :: MonadTCM tcm => tcm Term

primNatDivSucAux :: MonadTCM tcm => tcm Term

primNatModSucAux :: MonadTCM tcm => tcm Term

primNatEquality :: MonadTCM tcm => tcm Term

primNatLess :: MonadTCM tcm => tcm Term

primSize :: MonadTCM tcm => tcm Term

primSizeSuc :: MonadTCM tcm => tcm Term

primSizeInf :: MonadTCM tcm => tcm Term

primInf :: MonadTCM tcm => tcm Term

primSharp :: MonadTCM tcm => tcm Term

primFlat :: MonadTCM tcm => tcm Term

primEquality :: MonadTCM tcm => tcm Term

primRefl :: MonadTCM tcm => tcm Term

primLevel :: MonadTCM tcm => tcm Term

primLevelZero :: MonadTCM tcm => tcm Term

primLevelSuc :: MonadTCM tcm => tcm Term

primLevelMax :: MonadTCM tcm => tcm Term

primQName :: MonadTCM tcm => tcm Term

primArg :: MonadTCM tcm => tcm Term

primArgArg :: MonadTCM tcm => tcm Term

primAgdaTerm :: MonadTCM tcm => tcm Term

primAgdaTermVar :: MonadTCM tcm => tcm Term

primAgdaTermLam :: MonadTCM tcm => tcm Term

primAgdaTermDef :: MonadTCM tcm => tcm Term

primAgdaTermCon :: MonadTCM tcm => tcm Term

primAgdaTermPi :: MonadTCM tcm => tcm Term

primAgdaTermSort :: MonadTCM tcm => tcm Term

primAgdaTermUnsupported :: MonadTCM tcm => tcm Term

primInteger :: MonadTCM tcm => tcm Term

builtinTypes :: [String]