Changeset 1281 for src/LIN/LIN.ma
- Timestamp:
- Sep 28, 2011, 11:08:37 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LIN.ma
r1270 r1281 2 2 include "utilities/lists.ma". 3 3 4 definition lin_params_: params_ ≝ 5 mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) unit. 4 definition lin_params__: params__ ≝ 5 mk_params__ unit unit unit unit registers_move Register nat unit False. 6 definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit. 7 definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit. 8 definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit. 6 9 7 10 definition pre_lin_statement ≝ joint_statement lin_params_. … … 21 24 definition lin_params: ∀globals. params globals ≝ 22 25 λglobals. 23 mk_params globals lin_params_(Σcode:list (lin_statement globals). well_formed_P … code)26 mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code) 24 27 (λcode:Σcode.?. λl. 25 28 find ?? (λs. let 〈l',x〉 ≝ s in
Note: See TracChangeset
for help on using the changeset viewer.