Overview  Index  Help 

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.

           
Value summary

val stringOfExpression : ProofAst.expression -> string
           converts expression into string.

val stringOfProgram : bool -> bool -> ProofAst.program -> string list
           converts program into string accordingly to the formula/tex demand.

val stringOfProgram_Ott : ProofAst.program -> string list
           converts program into string, generating ott-oriented type and syntax.

val stringOfProgram_Untyped : bool -> bool -> ProofAst.program -> string list
           converts program into string accordingly to the formula/tex demand, without any type information.

 

       
Value detail

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.

 


Overview  Index  Help