Changeset 269 for Deliverables/D4.1
 Timestamp:
 Nov 23, 2010, 6:11:49 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Assembly.ma
r264 r269 3 3 ndefinition assembly1 ≝ 4 4 λ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 ] 7 13  _ ⇒ ? ]. 14 ##[##28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45: napply K; 15 ####47: 8 16 9 17 let (a10,a9,a8,b1) = from_word11 w in 
Deliverables/D4.1/Matita/BitVector.ma
r266 r269 70 70 append Bool m n b c. 71 71 72 interpretation "BitVector append" 'append b c = (append b c).73 74 72 ndefinition pad ≝ 75 73 λm, n: Nat. 
Deliverables/D4.1/Matita/Vector.ma
r268 r269 237 237 ]. 238 238 239 interpretation "Vector append" 'append hd tl = (append ? ? hd tl).239 interpretation "Vector append" 'append v1 v2 = (append ??? v1 v2). 240 240 241 241 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.