Overview  Index  Help 

PROOF_DERIV_PRETTY_PRINTER

All Known Implementing Modules:

ProofDerivPrettyPrinter


The First-Order LoopW Type Inference proof derivation pretty-printer. The proof derivation pretty-printer converts proof abstract syntax into string containing both program and typing derivation.

           
Value summary

val stringOfTyping
    : bool -> bool -> string list -> ProofAst.program -> string list

           converts program with typing derivation into string accordingly to the formula/tex demand.

 

       
Value detail

stringOfTyping

fun stringOfTyping form tex p
    : bool -> bool -> string list -> ProofAst.program -> string list

converts program with typing derivation into string accordingly to the formula/tex demand.

Parameters:
form
the formula-display (instead of imperative types) flag.
tex
the tex flag.
pr
the string representation of the untyped program.
p
the program.
Returns:
the string representation of p along with its partial typing derivation.

 


Overview  Index  Help