- 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
getBuiltin :: MonadTCM tcm => String -> tcm TermSource
getPrimitive :: MonadTCM tcm => String -> tcm PrimFunSource
The names of built-in things
primString :: 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
primSizeSuc :: MonadTCM tcm => tcm TermSource
primSizeInf :: MonadTCM tcm => tcm TermSource
primEquality :: MonadTCM tcm => tcm TermSource
primLevelZero :: MonadTCM tcm => tcm TermSource
primLevelSuc :: MonadTCM tcm => tcm TermSource
primLevelMax :: MonadTCM tcm => tcm TermSource
primInteger :: MonadTCM tcm => tcm TermSource
builtinTypes :: [String]Source