PROOF_PRETTY_PRINTER
- All Known Implementing Modules:
-
ProofPrettyPrinter
-
The First-Order LoopW Proof Checker proof syntax pretty-printer.
The proof pretty-printer converts proof abstract syntax into string.
-
stringOfProgram
fun stringOfProgram form tex p : bool -> bool -> ProofAst.program -> string list
-
converts program into string accordingly to the formula/tex demand.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
p
-
the program.
- Returns:
-
the string representation of p.
stringOfProgram_Ott
fun stringOfProgram_Ott p : ProofAst.program -> string list
-
converts program into string, generating ott-oriented type and syntax.
-
- Parameters:
-
-
p
-
the program.
- Returns:
-
the string representation of p.
stringOfProgram_Untyped
fun stringOfProgram_Untyped form tex p
: bool -> bool -> ProofAst.program -> string list
-
converts program into string accordingly to the formula/tex demand,
without any type information.
-
- Parameters:
-
-
form
-
the formula-disply (instead of imperative types) flag.
-
tex
-
the tex flag.
-
p
-
the program.
- Returns:
-
the string representation of p.
stringOfExpression
fun stringOfExpression e : ProofAst.expression -> string
-
converts expression into string.
-
- Parameters:
-
-
e
-
the expression.
- Returns:
-
the string representation of e.