- Timestamp:
- Apr 20, 2011, 11:33:35 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTLtoERTL.ma
r759 r763 118 118 ]. 119 119 120 definition fresh_register ≝ 121 λdef. 122 120 axiom fresh_reg: ertl_internal_function → ertl_internal_function × register. 121 122 let rec fresh_regs (def: ertl_internal_function) (n: nat) on n ≝ 123 match n with 124 [ O ⇒ 〈def, [ ]〉 125 | S n' ⇒ 126 let 〈def', regs'〉 ≝ fresh_regs def n' in 127 let 〈def', reg〉 ≝ fresh_reg def' in 128 〈def', reg :: regs'〉 129 ]. 130 131 definition save_hdws ≝ 132 λ
Note: See TracChangeset
for help on using the changeset viewer.