Changeset 283


Ignore:
Timestamp:
Nov 24, 2010, 11:01:24 PM (9 years ago)
Author:
sacerdot
Message:

Bug fixed in type declaration of BIT/N_BIT.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r278 r283  
    1818| INDIRECT_DPTR: addressing_mode
    1919| CARRY: addressing_mode
    20 | BIT_ADDR: Bit → addressing_mode
    21 | N_BIT_ADDR: Bit → addressing_mode
     20| BIT_ADDR: Byte → addressing_mode
     21| N_BIT_ADDR: Byte → addressing_mode
    2222| RELATIVE: Byte → addressing_mode
    2323| ADDR11: Word11 → addressing_mode
  • Deliverables/D4.1/Matita/Assembly.ma

    r282 r283  
    4949             | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    5050         ]
    51       | Right addrs ⇒ (*let 〈addr1,addr2〉 ≝ addrs in
     51      | Right addrs ⇒ let 〈addr1,addr2〉 ≝ addrs in
    5252         match addr2 return λx. bool_to_Prop (is_in ? [[bit_addr;n_bit_addr]] x) → ? with
    5353          [ BIT_ADDR b1 ⇒ λ_.[ ([[true;false;false;false;false;false;true;false]]) ; b1 ]
    5454          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
    55           | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]*) ?]
     55          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    5656 
    5757  | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
Note: See TracChangeset for help on using the changeset viewer.