- Timestamp:
- Jul 19, 2012, 2:42:02 PM (9 years ago)
- Location:
- src/LIN
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/LIN_paolo.ma
r2182 r2214 1 1 include "LIN/joint_LTL_LIN_paolo.ma". 2 2 3 definition lin_params ≝ mk_lin_params ltl_lin_params.3 definition LIN ≝ mk_lin_params LTL_LIN. 4 4 5 5 (* aid unification *) 6 6 unification hint 0 ≔ 7 7 (*---------------*) ⊢ 8 acc_a_reg lin_params≡ unit.8 acc_a_reg LIN ≡ unit. 9 9 unification hint 0 ≔ 10 10 (*---------------*) ⊢ 11 acc_a_arg lin_params≡ unit.11 acc_a_arg LIN ≡ unit. 12 12 unification hint 0 ≔ 13 13 (*---------------*) ⊢ 14 acc_b_reg lin_params≡ unit.14 acc_b_reg LIN ≡ unit. 15 15 unification hint 0 ≔ 16 16 (*---------------*) ⊢ 17 acc_a_arg lin_params≡ unit.17 acc_a_arg LIN ≡ unit. 18 18 unification hint 0 ≔ 19 19 (*---------------*) ⊢ 20 snd_arg lin_params ≡ ltl_argument.20 snd_arg LIN ≡ hdw_argument. 21 21 unification hint 0 ≔ 22 22 (*---------------*) ⊢ 23 ext_seq lin_params≡ ltl_lin_seq.23 ext_seq LIN ≡ ltl_lin_seq. 24 24 unification hint 0 ≔ 25 25 (*---------------*) ⊢ 26 pair_move lin_params≡ registers_move.26 pair_move LIN ≡ registers_move. 27 27 28 definition lin_program ≝ joint_program lin_params.28 definition lin_program ≝ joint_program LIN. -
src/LIN/joint_LTL_LIN_paolo.ma
r2208 r2214 12 12 | RESTORE_CARRY : ltl_lin_seq. 13 13 14 definition ltl_lin_params: unserialized_params ≝ mk_unserialized_params14 definition LTL_LIN : unserialized_params ≝ mk_unserialized_params 15 15 (mk_step_params 16 16 (* acc_a_reg ≝ *) unit
Note: See TracChangeset
for help on using the changeset viewer.