Changeset 269


Ignore:
Timestamp:
Nov 23, 2010, 6:11:49 PM (9 years ago)
Author:
sacerdot
Message:
  • ...
Location:
Deliverables/D4.1/Matita
Files:
3 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
  • Deliverables/D4.1/Matita/BitVector.ma

    r266 r269  
    7070    append Bool m n b c.
    7171   
    72 interpretation "BitVector append" 'append b c = (append b c).
    73 
    7472ndefinition pad ≝
    7573  λm, n: Nat.
  • Deliverables/D4.1/Matita/Vector.ma

    r268 r269  
    237237    ].
    238238   
    239 interpretation "Vector append" 'append hd tl = (append ? ? hd tl).
     239interpretation "Vector append" 'append v1 v2 = (append ??? v1 v2).
    240240   
    241241nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset for help on using the changeset viewer.