tip-lib-0.2.2: tons of inductive problems - support library and tools

Safe Haskell	None
Language	Haskell2010

Tip.Pretty.TFF

Documentation

apply :: Doc -> [Doc] -> Doc Source

clause :: String -> String -> Doc -> Doc Source

validTFFChar :: Char -> String Source

ppTheory :: (Ord a, PrettyVar a) => Theory a -> Doc Source

ppSort :: PrettyVar a => Sort a -> Doc Source

ppUninterp :: PrettyVar a => Signature a -> Doc Source

ppFormula :: (Ord a, PrettyVar a) => Formula a -> Doc Source

tffify :: Ord a => Expr a -> Expr a Source

tffvarify :: Ord a => Theory a -> Theory (Why3Var a) Source

ppExpr :: (Ord a, PrettyVar a) => Int -> Expr a -> Doc Source

ppLocal :: PrettyVar a => Local a -> Doc Source

ppQuant :: Quant -> Doc Source

ppHead :: PrettyVar a => Head a -> Doc Source

ppBuiltin :: Builtin -> Doc Source

ppLit :: Lit -> Doc Source

ppType :: PrettyVar a => Type a -> Doc Source

ppBuiltinType :: BuiltinType -> Doc Source