| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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
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
primInteger :: MonadTCM tcm => tcm Term
builtinTypes :: [String]

Documentation

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

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

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

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

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

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

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

The names of built-in things

primFloat :: MonadTCM tcm => tcm Term | Source

primChar :: MonadTCM tcm => tcm Term | Source

primString :: MonadTCM tcm => tcm Term | Source

primBool :: MonadTCM tcm => tcm Term | Source

primTrue :: MonadTCM tcm => tcm Term | Source

primFalse :: MonadTCM tcm => tcm Term | Source

primList :: MonadTCM tcm => tcm Term | Source

primNil :: MonadTCM tcm => tcm Term | Source

primCons :: MonadTCM tcm => tcm Term | Source

primIO :: MonadTCM tcm => tcm Term | Source

primNat :: MonadTCM tcm => tcm Term | Source

primSuc :: MonadTCM tcm => tcm Term | Source

primZero :: MonadTCM tcm => tcm Term | Source

primNatPlus :: MonadTCM tcm => tcm Term | Source

primNatMinus :: MonadTCM tcm => tcm Term | Source

primNatTimes :: MonadTCM tcm => tcm Term | Source

primNatDivSucAux :: MonadTCM tcm => tcm Term | Source

primNatModSucAux :: MonadTCM tcm => tcm Term | Source

primNatEquality :: MonadTCM tcm => tcm Term | Source

primNatLess :: MonadTCM tcm => tcm Term | Source

primSize :: MonadTCM tcm => tcm Term | Source

primSizeSuc :: MonadTCM tcm => tcm Term | Source

primSizeInf :: MonadTCM tcm => tcm Term | Source

primEquality :: MonadTCM tcm => tcm Term | Source

primRefl :: MonadTCM tcm => tcm Term | Source

primLevel :: MonadTCM tcm => tcm Term | Source

primLevelZero :: MonadTCM tcm => tcm Term | Source

primLevelSuc :: MonadTCM tcm => tcm Term | Source

primLevelMax :: MonadTCM tcm => tcm Term | Source

primInteger :: MonadTCM tcm => tcm Term | Source

builtinTypes :: [String] | Source

Produced by Haddock version 2.4.2