Changeset 712 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Mar 28, 2011, 5:40:51 PM (9 years ago)
Author:
mulligan
Message:

Changes to get things to typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r698 r712  
    7575qed.
    7676
    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.
     77definition 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 *)
     82qed.
     83
     84definition 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 *)
     90qed.
     91
     92definition 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 *)
     97qed.
     98
     99definition 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 *)
     105qed.
    81106
    82107definition increment ≝
Note: See TracChangeset for help on using the changeset viewer.