This module defines pretty printers for
Note that the printers for terms and theorems are context dependent as they
rely on the same theory extensions that the parsers utilize.
To make printing these objects easier within HOL computations, this module
also defines the
printHOL methods which will automatically
retrieve the current working theory to use for pretty printing. Because the
pretty printer for
HOLTypes is not context dependent it has definitions for
Note that, like the parser, there are a number of HOL term forms that the printer does not currently support. Again, these are mainly related to sets and patterns and will be added in when the HaskHOL system has libraries for them.
- data FlagRevInterface = FlagRevInterface
- data FlagPrintAllThm = FlagPrintAllThm
- addUnspacedBinop :: String -> HOL Theory thry ()
- addPrebrokenBinop :: String -> HOL Theory thry ()
- removeUnspacedBinop :: String -> HOL Theory thry ()
- removePrebrokenBinop :: String -> HOL Theory thry ()
- getUnspacedBinops :: HOLContext thry -> [String]
- getPrebrokenBinops :: HOLContext thry -> [String]
- ppType :: HOLType -> String
- ppTerm :: HOLContext thry -> HOLTerm -> String
- ppThm :: HOLContext thry -> HOLThm -> String
- class ShowHOL a thry where
- printHOL :: ShowHOL a thry => a -> HOL cls thry ()
Pretty Printer Flags
Flag to indicate whether the interface should be reversed on printing.
Flag to indicate if the entirety of a theorem should be printed, as opposed to just the conclusion term.
Extensible Printer Operators
Specifies a symbol to be recognized as a prebroken, binary operator by the
printer. Applications involving these operators will have their right-hand
side argument printed on the next line using the
Returns the list of all symbols current recognized as unspaced, binary operators by the printer.
Returns the list of all symbols current recognized as prebroken, binary operators by the printer.
Printing in the
ShowHOL class is functionally equivalent to
show lifted to the
monad. It is used to retrieve the current working theory to be used with the
context sensitive pretty printers for
|ShowHOL String thry|
|ShowHOL Assoc thry|
|ShowHOL HOLThm thry|
|ShowHOL HOLTerm thry|
|ShowHOL TypeOp thry|
|ShowHOL HOLType thry|
|ShowHOL a thry => ShowHOL [a] thry|
|(ShowHOL a thry, ShowHOL b thry) => ShowHOL (a, b) thry|
|(ShowHOL a thry, ShowHOL b thry, ShowHOL c thry) => ShowHOL (a, b, c) thry|
|(ShowHOL a thry, ShowHOL b thry, ShowHOL c thry, ShowHOL d thry) => ShowHOL (a, b, c, d) thry|