Changeset 308 for Deliverables
 Timestamp:
 Nov 26, 2010, 12:49:08 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r307 r308 165 165 [ DATA b2 ⇒ λ_. b2 166 166  _ ⇒ λ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) ]] 175 173  INC addr ⇒ 176 174 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.