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