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

Agda.TypeChecking.Monad.Builtin

Contents

Synopsis

Documentation

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)

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

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

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

primInteger :: MonadTCM tcm => tcm Term