Changeset 308


Ignore:
Timestamp:
Nov 26, 2010, 12:49:08 AM (9 years ago)
Author:
sacerdot
Message:

More explicit typing solves one of the points.

File:
1 edited

Legend:

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

    r307 r308  
    165165               [ DATA b2 ⇒ λ_. b2
    166166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    167 
    168 [ ] (*
    169              match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
    170               [ REGISTER r1 r2 r3 ⇒ λ_. [](*
    171                  [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]*)
    172               | INDIRECT i1 ⇒ λ_. [] (*
    173                  [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] *)
    174               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)*) ]]
     167             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → List Byte with
     168              [ REGISTER r1 r2 r3 ⇒ λ_.
     169                 [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]
     170              | INDIRECT i1 ⇒ λ_.
     171                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ]
     172              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1) ]]
    175173  | INC addr ⇒
    176174     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect;dptr]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.