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

Safe Haskell	None
Language	Haskell2010

Tip.Pretty.Why3

Documentation

data Why3Var a Source

Constructors

Instances

Eq a => Eq (Why3Var a) Source
Ord a => Ord (Why3Var a) Source
Show a => Show (Why3Var a) Source
PrettyVar a => PrettyVar (Why3Var a) Source

why3VarTheory :: forall a. Ord a => Theory a -> Theory (Why3Var a) Source

block :: Doc -> Doc -> Doc Source

pcsv :: [Doc] -> Doc Source

csv :: [Doc] -> Doc Source

csv1 :: [Doc] -> Doc Source

separating :: ([Doc] -> Doc) -> [Doc] -> [Doc] -> Doc Source

escape :: Char -> String Source

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

ppSort :: (PrettyVar a, Ord a) => Sort a -> Doc Source

ppDatas :: (PrettyVar a, Ord a) => [Datatype a] -> Doc Source

ppData :: (PrettyVar a, Ord a) => Doc -> Datatype a -> Doc Source

ppCon :: (PrettyVar a, Ord a) => Constructor a -> Doc Source

ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> Doc Source

ppBinder :: (PrettyVar a, Ord a) => a -> Type a -> Doc Source

ppLocalBinder :: (PrettyVar a, Ord a) => Local a -> Doc Source

ppUninterp :: (PrettyVar a, Ord a) => Signature a -> Doc Source

ppFuncs :: (PrettyVar a, Ord a) => [Function a] -> Doc Source

ppFunc :: (PrettyVar a, Ord a) => Doc -> Function a -> Doc Source

ppDeepPattern :: PrettyVar a => DeepPattern a -> Doc Source

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

ppRole :: Role -> Doc Source

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

ppHead :: (PrettyVar a, Ord a) => Head a -> [Doc] -> Doc Source

ppBuiltin :: Builtin -> Doc Source

ppBinOp :: Builtin -> Maybe Doc Source

ppLit :: Lit -> Doc Source

ppQuantName :: Quant -> Doc Source

ppCase :: (PrettyVar a, Ord a) => Case a -> Doc Source

ppPat :: (PrettyVar a, Ord a) => Pattern a -> Doc Source

ppType :: (PrettyVar a, Ord a) => Int -> Type a -> Doc Source

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

why3Keywords :: [String] Source