Changeset 712 for src/ASM/Arithmetic.ma
- Timestamp:
- Mar 28, 2011, 5:40:51 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r698 r712 75 75 qed. 76 76 77 definition add_8_with_carry ≝ add_n_with_carry 8. 78 definition add_16_with_carry ≝ add_n_with_carry 16. 79 definition sub_8_with_carry ≝ sub_n_with_carry 8. 80 definition sub_16_with_carry ≝ sub_n_with_carry 16. 77 definition add_8_with_carry ≝ 78 λb, c: BitVector 8. 79 λcarry: bool. 80 add_n_with_carry 8 b c carry ?. 81 @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) 82 qed. 83 84 definition add_16_with_carry ≝ 85 λb, c: BitVector 16. 86 λcarry: bool. 87 add_n_with_carry 16 b c carry ?. 88 @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S 89 @le_S @le_S @le_n (* ugly: fix using tacticals *) 90 qed. 91 92 definition sub_8_with_carry ≝ 93 λb, c: BitVector 8. 94 λcarry: bool. 95 sub_n_with_carry 8 b c carry ?. 96 @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *) 97 qed. 98 99 definition sub_16_with_carry ≝ 100 λb, c: BitVector 16. 101 λcarry: bool. 102 sub_n_with_carry 16 b c carry ?. 103 @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S 104 @le_S @le_S @le_n (* ugly: fix using tacticals *) 105 qed. 81 106 82 107 definition increment ≝
Note: See TracChangeset
for help on using the changeset viewer.