- Timestamp:
- May 24, 2012, 7:18:35 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLToERTL.ma
r1601 r1995 4 4 include "ERTL/ERTL.ma". 5 5 include "joint/TranslateUtils.ma". 6 7 include alias "basics/lists/list.ma". 6 8 7 9 definition save_hdws ≝ … … 412 414 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)). 413 415 414 definition translate: rtl_program → ertl_program ≝416 definition rtl_to_ertl : rtl_program → ertl_program ≝ 415 417 λp. 416 418 let p ≝ tailcall_simplify p in (* tailcall simplification here *)
Note: See TracChangeset
for help on using the changeset viewer.