Skip to content

137 translator simulations, dep_comb_witness1_eq and dep_parse_comparable_data_eq

Andrey Klaus requested to merge ak@137-translator-simulations-40-49-48-49 into master
  • dep_comb_witness1_eq and dep_parse_comparable_data_eq are proved.
  • move 2 lemmas from Proofs/Script_ir_translator.v to Proofs/Script_typed_ir.v.
  • minor code cleanups
Edited by Andrey Klaus

Merge request reports