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.