Safe Haskell	None
Language	Haskell2010

HOL.Print

Description

Documentation

isSymbolChar :: Char -> Bool Source #

isSymbolString :: String -> Bool Source #

ppSymbolName :: Name -> Doc Source #

type PrefixOp = Doc -> Doc Source #

ppPrefixOps :: [PrefixOp] -> Doc -> Doc Source #

type Prec = Int Source #

data Assoc Source #

Constructors

LeftAssoc
RightAssoc
NonAssoc

Instances

Instances details

Eq Assoc Source #
Instance details Defined in HOL.Print Methods (==) :: Assoc -> Assoc -> Bool # (/=) :: Assoc -> Assoc -> Bool #
Ord Assoc Source #
Instance details Defined in HOL.Print Methods compare :: Assoc -> Assoc -> Ordering # (<) :: Assoc -> Assoc -> Bool # (<=) :: Assoc -> Assoc -> Bool # (>) :: Assoc -> Assoc -> Bool # (>=) :: Assoc -> Assoc -> Bool # max :: Assoc -> Assoc -> Assoc # min :: Assoc -> Assoc -> Assoc #
Show Assoc Source #
Instance details Defined in HOL.Print Methods showsPrec :: Int -> Assoc -> ShowS # show :: Assoc -> String # showList :: [Assoc] -> ShowS #

type InfixOp = (Prec, Assoc, Doc -> Doc) Source #

ppInfixOps :: (a -> Maybe (InfixOp, a, a)) -> (Bool -> a -> Doc) -> Bool -> a -> Doc Source #

class Printable a where Source #

Minimal complete definition

toDoc

Methods

toDoc :: a -> Doc Source #

toStringWith :: Style -> a -> String Source #

toString :: a -> String Source #

Instances

Instances details

Printable Integer Source #
Instance details Defined in HOL.Print Methods toDoc :: Integer -> Doc Source # toStringWith :: Style -> Integer -> String Source # toString :: Integer -> String Source #
Printable Doc Source #
Instance details Defined in HOL.Print Methods toDoc :: Doc -> Doc Source # toStringWith :: Style -> Doc -> String Source # toString :: Doc -> String Source #
Printable Name Source #
Instance details Defined in HOL.Print Methods toDoc :: Name -> Doc Source # toStringWith :: Style -> Name -> String Source # toString :: Name -> String Source #
Printable Namespace Source #
Instance details Defined in HOL.Print Methods toDoc :: Namespace -> Doc Source # toStringWith :: Style -> Namespace -> String Source # toString :: Namespace -> String Source #
Printable Term Source #
Instance details Defined in HOL.Print Methods toDoc :: Term -> Doc Source # toStringWith :: Style -> Term -> String Source # toString :: Term -> String Source #
Printable Const Source #
Instance details Defined in HOL.Print Methods toDoc :: Const -> Doc Source # toStringWith :: Style -> Const -> String Source # toString :: Const -> String Source #
Printable Var Source #
Instance details Defined in HOL.Print Methods toDoc :: Var -> Doc Source # toStringWith :: Style -> Var -> String Source # toString :: Var -> String Source #
Printable Type Source #
Instance details Defined in HOL.Print Methods toDoc :: Type -> Doc Source # toStringWith :: Style -> Type -> String Source # toString :: Type -> String Source #
Printable TypeOp Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeOp -> Doc Source # toStringWith :: Style -> TypeOp -> String Source # toString :: TypeOp -> String Source #
Printable TypeVar Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeVar -> Doc Source # toStringWith :: Style -> TypeVar -> String Source # toString :: TypeVar -> String Source #
Printable TypeSubst Source #
Instance details Defined in HOL.Print Methods toDoc :: TypeSubst -> Doc Source # toStringWith :: Style -> TypeSubst -> String Source # toString :: TypeSubst -> String Source #
Printable TermAlpha Source #
Instance details Defined in HOL.Print Methods toDoc :: TermAlpha -> Doc Source # toStringWith :: Style -> TermAlpha -> String Source # toString :: TermAlpha -> String Source #
Printable Sequent Source #
Instance details Defined in HOL.Print Methods toDoc :: Sequent -> Doc Source # toStringWith :: Style -> Sequent -> String Source # toString :: Sequent -> String Source #
Printable Thm Source #
Instance details Defined in HOL.Print Methods toDoc :: Thm -> Doc Source # toStringWith :: Style -> Thm -> String Source # toString :: Thm -> String Source #
Printable Theory Source #
Instance details Defined in HOL.Theory Methods toDoc :: Theory -> Doc Source # toStringWith :: Style -> Theory -> String Source # toString :: Theory -> String Source #
Printable Interpret Source #
Instance details Defined in HOL.OpenTheory.Interpret Methods toDoc :: Interpret -> Doc Source # toStringWith :: Style -> Interpret -> String Source # toString :: Interpret -> String Source #
Printable Renames Source #
Instance details Defined in HOL.OpenTheory.Interpret Methods toDoc :: Renames -> Doc Source # toStringWith :: Style -> Renames -> String Source # toString :: Renames -> String Source #
Printable Rename Source #
Instance details Defined in HOL.OpenTheory.Interpret Methods toDoc :: Rename -> Doc Source # toStringWith :: Style -> Rename -> String Source # toString :: Rename -> String Source #
Printable Symbol Source #
Instance details Defined in HOL.OpenTheory.Interpret Methods toDoc :: Symbol -> Doc Source # toStringWith :: Style -> Symbol -> String Source # toString :: Symbol -> String Source #
Printable State Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: State -> Doc Source # toStringWith :: Style -> State -> String Source # toString :: State -> String Source #
Printable Command Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Command -> Doc Source # toStringWith :: Style -> Command -> String Source # toString :: Command -> String Source #
Printable Object Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Object -> Doc Source # toStringWith :: Style -> Object -> String Source # toString :: Object -> String Source #
Printable Number Source #
Instance details Defined in HOL.OpenTheory.Article Methods toDoc :: Number -> Doc Source # toStringWith :: Style -> Number -> String Source # toString :: Number -> String Source #
Printable Package Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Package -> Doc Source # toStringWith :: Style -> Package -> String Source # toString :: Package -> String Source #
Printable Block Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Block -> Doc Source # toStringWith :: Style -> Block -> String Source # toString :: Block -> String Source #
Printable File Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: File -> Doc Source # toStringWith :: Style -> File -> String Source # toString :: File -> String Source #
Printable Info Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Info -> Doc Source # toStringWith :: Style -> Info -> String Source # toString :: Info -> String Source #
Printable KeyValue Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: KeyValue -> Doc Source # toStringWith :: Style -> KeyValue -> String Source # toString :: KeyValue -> String Source #
Printable NameVersion Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: NameVersion -> Doc Source # toStringWith :: Style -> NameVersion -> String Source # toString :: NameVersion -> String Source #
Printable Version Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Version -> Doc Source # toStringWith :: Style -> Version -> String Source # toString :: Version -> String Source #
Printable Name Source #
Instance details Defined in HOL.OpenTheory.Package Methods toDoc :: Name -> Doc Source # toStringWith :: Style -> Name -> String Source # toString :: Name -> String Source #
Printable a => Printable [a] Source #
Instance details Defined in HOL.Print Methods toDoc :: [a] -> Doc Source # toStringWith :: Style -> [a] -> String Source # toString :: [a] -> String Source #
Printable a => Printable (Set a) Source #
Instance details Defined in HOL.Print Methods toDoc :: Set a -> Doc Source # toStringWith :: Style -> Set a -> String Source # toString :: Set a -> String Source #
(Printable a, Printable b) => Printable (a, b) Source #
Instance details Defined in HOL.Print Methods toDoc :: (a, b) -> Doc Source # toStringWith :: Style -> (a, b) -> String Source # toString :: (a, b) -> String Source #

quoteNamespace :: Namespace -> Doc Source #

quoteName :: Name -> Doc Source #