Ignore:
Timestamp:
Nov 26, 2010, 3:24:16 PM (9 years ago)
Author:
sacerdot
Message:

arguments of split reversed

File:
1 edited

Legend:

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

    r309 r312  
    66     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    77      [ ADDR11 w ⇒ λ_.
    8          let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
     8         let 〈v1,v2〉 ≝ split ? (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
    99          [ (v1 @@ [[true; false; false; false; true]]) ; v2 ]
    1010      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     
    2626     match addr return λx. bool_to_Prop (is_in ? [[addr11]] x) → ? with
    2727      [ ADDR11 w ⇒ λ_.
    28          let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in
     28         let 〈v1,v2〉 ≝ split ?  (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))) w in
    2929          [ (v1 @@ [[false; false; false; false; true]]) ; v2 ]
    3030      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
Note: See TracChangeset for help on using the changeset viewer.