Tip.Haskell.Translate

Contents

• Builtins
• QuickSpec signatures

Synopsis

• prelude :: String -> HsId a
• tipDSL :: String -> HsId a
• quickCheck :: String -> HsId a
• quickCheckUnsafe :: String -> HsId a
• quickCheckAll :: String -> HsId a
• quickSpec :: String -> HsId a
• sysEnv :: String -> HsId a
• smtenSym :: String -> HsId a
• smtenEnv :: String -> HsId a
• smtenMinisat :: String -> HsId a
• smtenMonad :: String -> HsId a
• feat :: String -> HsId a
• lsc :: String -> HsId a
• typeable :: String -> HsId a
• data HsId a
  • = Qualified {
    • qual_module :: String
    • qual_module_short :: Maybe String
    • qual_func :: String
    }
  • | Exact String
  • | Other a
  • | Derived (HsId a) String
• addHeader :: String -> Decls a -> Decls a
• addImports :: Ord a => Decls (HsId a) -> Decls (HsId a)
• trTheory :: (Ord a, PrettyVar a) => Mode -> Theory a -> Decls (HsId a)
• data Kind
  • = Expr
  • | Formula
• theorySigs :: Theory (HsId a) -> [HsId a]
• ufInfo :: Theory (HsId a) -> (Bool, [Type (HsId a)])
• data Mode
  • = Feat
  • | QuickCheck
  • | LazySmallCheck Bool
  • | Smten
  • | QuickSpec
  • | Plain
• isLazySmallCheck :: Mode -> Bool
• isSmten :: Mode -> Bool
• trTheory' :: forall a b. (a ~ HsId b, Ord b, PrettyVar b) => Mode -> Theory a -> Decls a
• arbitrary :: [Type (HsId a)] -> [Type (HsId a)]
• trType :: (a ~ HsId b) => Type a -> Type a
• trBuiltinType :: BuiltinType -> Type (HsId a)
• withBool :: (a ~ HsId b) => (a -> [c] -> d) -> Bool -> d
• hsBuiltinTys :: [(BuiltinType, String)]
• hsBuiltins :: [(Builtin, String)]
• typeOfBuiltin :: Builtin -> Type a
• makeSig :: forall a. (PrettyVar a, Ord a) => Theory (HsId a) -> Decl (HsId a)
• theoryBuiltins :: Ord a => Theory a -> [Builtin]

Documentation

Builtins

QuickSpec signatures