Ignore:
Timestamp:
Nov 23, 2010, 6:11:49 PM (10 years ago)
Author:
sacerdot
Message:
  • ...
File:
1 edited

Legend:

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

    r264 r269  
    33ndefinition assembly1 ≝
    44 λi.match i with
    5   [ ACALL (ADDR11 w) ⇒
    6      
     5  [ ACALL addr ⇒
     6     let w ≝
     7      match addr with [ mk_subaddressing_mode addr1 proof1 ⇒
     8       match addr1 return λx.∀proof: bool_to_Prop (is_in ?? x).? with
     9        [ ADDR11 w ⇒ λ_.w | _ ⇒ λK.⊥ ] proof1] in
     10     match split ?? (S (S (S (S (S (S (S (S Z)))))))) w with
     11      [ mk_Cartesian v1 v2 ⇒
     12         v1 @ [[true; false; false; false; true]] @ v2 ]
    713  | _ ⇒ ? ].
     14##[##28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45: napply K;
     15##|##47:
    816 
    917      let (a10,a9,a8,b1) = from_word11 w in
Note: See TracChangeset for help on using the changeset viewer.