Agda.TypeChecking.Monad.Builtin

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]