Overview  Index  Help 

FUN_TRANSLATION

All Known Implementing Modules:

FunTranslation


The First-Order LoopW Proof Checker translator into functional syntax. The functional translator converts imperative programs into functional terms.

           
Value summary

val translateProgram : ProofAst.sequence -> FunAst.typed_term
           translate a complete imperative program into a functional typed term.

 

       
Value detail

translateProgram

fun translateProgram p : ProofAst.sequence -> FunAst.typed_term

translate a complete imperative program into a functional typed term.

Parameters:
p
the imperative program.
Returns:
the functional term p*.

 


Overview  Index  Help