Ignore:
Timestamp:
Dec 2, 2010, 5:13:22 PM (9 years ago)
Author:
mulligan
Message:

Added decidable equality for addressing_mode_tags.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/ASM.ma

    r357 r367  
    4444| addr11: addressing_mode_tag
    4545| addr16: addressing_mode_tag.
     46
     47ndefinition eq_a ≝
     48  λa, b: addressing_mode_tag.
     49    match a with
     50      [ direct ⇒ match b with [ direct ⇒ true | _ ⇒ false ]
     51      | indirect ⇒ match b with [ indirect ⇒ true | _ ⇒ false ]
     52      | ext_indirect ⇒ match b with [ ext_indirect ⇒ true | _ ⇒ false ]
     53      | register ⇒ match b with [ register ⇒ true | _ ⇒ false ]
     54      | acc_a ⇒ match b with [ acc_a ⇒ true | _ ⇒ false ]
     55      | acc_b ⇒ match b with [ acc_b ⇒ true | _ ⇒ false ]
     56      | dptr ⇒ match b with [ dptr ⇒ true | _ ⇒ false ]
     57      | data ⇒ match b with [ data ⇒ true | _ ⇒ false ]
     58      | data16 ⇒ match b with [ data16 ⇒ true | _ ⇒ false ]
     59      | acc_dptr ⇒ match b with [ acc_dptr ⇒ true | _ ⇒ false ]
     60      | acc_pc ⇒ match b with [ acc_pc ⇒ true | _ ⇒ false ]
     61      | ext_indirect_dptr ⇒ match b with [ ext_indirect_dptr ⇒ true | _ ⇒ false ]
     62      | indirect_dptr ⇒ match b with [ indirect_dptr ⇒ true | _ ⇒ false ]
     63      | carry ⇒ match b with [ carry ⇒ true | _ ⇒ false ]
     64      | bit_addr ⇒ match b with [ bit_addr ⇒ true | _ ⇒ false ]
     65      | n_bit_addr ⇒ match b with [ n_bit_addr ⇒ true | _ ⇒ false ]
     66      | relative ⇒ match b with [ relative ⇒ true | _ ⇒ false ]
     67      | addr11 ⇒ match b with [ addr11 ⇒ true | _ ⇒ false ]
     68      | addr16 ⇒ match b with [ addr16 ⇒ true | _ ⇒ false ]
     69      ].
    4670
    4771(* to avoid expansion... *)
Note: See TracChangeset for help on using the changeset viewer.