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/Interpret.ma

    r364 r367  
    88naxiom eq_a: addressing_mode_tag → addressing_mode_tag → Bool.
    99   
    10 nlemma execute_1_technical:
     10naxiom execute_1_technical:
    1111  ∀n,m: Nat.
    1212  ∀v: Vector addressing_mode_tag (S n).
     
    1616    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
    1717    bool_to_Prop (is_in ? q a).
    18   #n m v q a.
    19   ncases a.
    20   nnormalize.
    2118   
    2219ndefinition execute_1: Status → Status ≝
     
    512509          nnormalize
    513510          //);
    514     ##|
     511    ##| napply (execute_1_technical ? ? [[ acc_a ]]
     512                                        [[ direct; indirect; register;
     513                                           acc_a; acc_b; data; acc_dptr;
     514                                           acc_pc; ext_indirect;
     515                                           ext_indirect_dptr ]] ACC_A).
    515516nqed.
    516517
Note: See TracChangeset for help on using the changeset viewer.