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

Safe Haskell	None
Language	Haskell2010

Tip.Pretty.Isabelle

Documentation

($-$) :: Doc -> Doc -> Doc 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

intersperseWithPre :: (a -> a -> a) -> a -> [a] -> [a] Source

quote :: Doc -> Doc Source

quoteWhen :: (a -> Bool) -> a -> Doc -> Doc Source

ppAsTuple :: [a] -> (a -> Doc) -> Doc 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) => Datatype a -> Doc Source

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

ppQuant :: (PrettyVar a, Ord a) => Doc -> [Local a] -> Doc -> 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) => Function a -> (Doc, [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

isabelleKeywords :: [String] Source