Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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)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 TermSource
getBuiltin' :: MonadTCM tcm => String -> tcm (Maybe Term)Source
getPrimitive :: MonadTCM tcm => String -> tcm PrimFunSource
The names of built-in things
primFloat :: MonadTCM tcm => tcm TermSource
primChar :: MonadTCM tcm => tcm TermSource
primString :: MonadTCM tcm => tcm TermSource
primBool :: MonadTCM tcm => tcm TermSource
primTrue :: MonadTCM tcm => tcm TermSource
primFalse :: MonadTCM tcm => tcm TermSource
primList :: MonadTCM tcm => tcm TermSource
primNil :: MonadTCM tcm => tcm TermSource
primCons :: MonadTCM tcm => tcm TermSource
primIO :: MonadTCM tcm => tcm TermSource
primNat :: MonadTCM tcm => tcm TermSource
primSuc :: MonadTCM tcm => tcm TermSource
primZero :: MonadTCM tcm => tcm TermSource
primNatPlus :: MonadTCM tcm => tcm TermSource
primNatMinus :: MonadTCM tcm => tcm TermSource
primNatTimes :: MonadTCM tcm => tcm TermSource
primNatDivSucAux :: MonadTCM tcm => tcm TermSource
primNatModSucAux :: MonadTCM tcm => tcm TermSource
primNatEquality :: MonadTCM tcm => tcm TermSource
primNatLess :: MonadTCM tcm => tcm TermSource
primSize :: MonadTCM tcm => tcm TermSource
primSizeSuc :: MonadTCM tcm => tcm TermSource
primSizeInf :: MonadTCM tcm => tcm TermSource
primInf :: MonadTCM tcm => tcm TermSource
primSharp :: MonadTCM tcm => tcm TermSource
primFlat :: MonadTCM tcm => tcm TermSource
primEquality :: MonadTCM tcm => tcm TermSource
primRefl :: MonadTCM tcm => tcm TermSource
primLevel :: MonadTCM tcm => tcm TermSource
primLevelZero :: MonadTCM tcm => tcm TermSource
primLevelSuc :: MonadTCM tcm => tcm TermSource
primLevelMax :: MonadTCM tcm => tcm TermSource
primQName :: MonadTCM tcm => tcm TermSource
primArg :: MonadTCM tcm => tcm TermSource
primArgArg :: MonadTCM tcm => tcm TermSource
primAgdaTerm :: MonadTCM tcm => tcm TermSource
primAgdaTermVar :: MonadTCM tcm => tcm TermSource
primAgdaTermLam :: MonadTCM tcm => tcm TermSource
primAgdaTermDef :: MonadTCM tcm => tcm TermSource
primAgdaTermCon :: MonadTCM tcm => tcm TermSource
primAgdaTermPi :: MonadTCM tcm => tcm TermSource
primAgdaTermSort :: MonadTCM tcm => tcm TermSource
primAgdaTermUnsupported :: MonadTCM tcm => tcm TermSource
primInteger :: MonadTCM tcm => tcm TermSource
builtinTypes :: [String]Source
Produced by Haddock version 2.6.1