Changeset 3037 for src/RTL/RTL.ma
- Timestamp:
- Mar 29, 2013, 5:19:53 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/RTL/RTL.ma
r2975 r3037 93 93 94 94 (* parameters for main need to be passed to the premain *) 95 definition RTL_premain : ∀p : rtl_program.joint_closed_internal_function RTL (prog_var_names ?? p) ≝ 95 definition RTL_premain : ∀p : rtl_program. 96 joint_closed_internal_function RTL (prog_names … p) ≝ 96 97 λp. 97 98 let l1 : label ≝ an_identifier … one in … … 104 105 an_identifier … (p0 (p0 one)) ] in 105 106 let res ≝ 106 mk_joint_internal_function RTL (prog_ var_names … p)107 mk_joint_internal_function RTL (prog_names … p) 107 108 (mk_universe … (p0 (p0 one))) 108 109 (mk_universe … (p1 (p0 one)))
Note: See TracChangeset
for help on using the changeset viewer.