Changeset 712 for src/ASM/Arithmetic.ma

Timestamp:

Mar 28, 2011, 5:40:51 PM (9 years ago)

Author:

mulligan

Message:

Changes to get things to typecheck.

File:

• src/ASM/Arithmetic.ma (modified) (1 diff)

src/ASM/Arithmetic.ma

@@ -75 +75 @@
 qed.
 
-definition add_8_with_carry ≝ add_n_with_carry 8.
-definition add_16_with_carry ≝ add_n_with_carry 16.
-definition sub_8_with_carry ≝ sub_n_with_carry 8.
-definition sub_16_with_carry ≝ sub_n_with_carry 16.
+definition add_8_with_carry ≝
+  λb, c: BitVector 8.
+  λcarry: bool.
+  add_n_with_carry 8 b c carry ?.
+  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
+qed.
+
+definition add_16_with_carry ≝
+  λb, c: BitVector 16.
+  λcarry: bool.
+  add_n_with_carry 16 b c carry ?.
+  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
+  @le_S @le_S @le_n (* ugly: fix using tacticals *)
+qed.
+
+definition sub_8_with_carry ≝
+  λb, c: BitVector 8.
+  λcarry: bool.
+  sub_n_with_carry 8 b c carry ?.
+  @le_S @le_S @le_S @le_n (* ugly: fix using tacticals *)
+qed.
+
+definition sub_16_with_carry ≝
+  λb, c: BitVector 16.
+  λcarry: bool.
+  sub_n_with_carry 16 b c carry ?.
+  @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S @le_S
+  @le_S @le_S @le_n (* ugly: fix using tacticals *)
+qed.
 
 definition increment ≝