Changeset 272 for Deliverables/D4.1/Matita
 Timestamp:
 Nov 24, 2010, 1:43:28 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Arithmetic.ma
r260 r272 62 62 nqed. 63 63 64 (* 64 naxiom less_than_b: Nat → Nat → Bool. 65 65 66 ndefinition sub_8_with_carry ≝ 66 67 λb: BitVector eight. … … 70 71 let c_as_nat ≝ nat_of_bitvector eight c in 71 72 let carry_as_nat ≝ nat_of_bool carry in 72 let result_old_1 ≝ subtraction_underflow b_as_nat c_as_nat in 73 match result_old_1 with 74 [ Nothing ⇒ 75 let ac_flag ≝ True in 76 77  Just result_old_1' ⇒ 78 ] 79 *) 73 let result_old_1 ≝ minus (minus b_as_nat c_as_nat) carry_as_nat in 74 let modulus_1 ≝ (modulus b_as_nat sixteen)  (modulus c_as_nat sixteen) in 75 match less_than_b (modulus b_as_nat sixteen) (modulus c_as_nat sixteen) with 76 [ true ⇒ 77 let ac_flag ≝ true in 78 let result_old_2 ≝ (minus (modulus b_as_nat one_hundred_and_twenty_eight) 79 (modulus c_as_nat one_hundred_and_twenty_eight)) in 80 match less_than_b (modulus b_as_nat one_hundred_and_twenty_eight) 81 (modulus c_as_nat one_hundred_and_twenty_eight) with 82 [ true ⇒ 83 let bit_six ≝ true in 84 let result_carry ≝ mk_Cartesian … result_old_1 false in 85 let ov_flag ≝ exclusive_disjunction cy_flag bit_six in 86 mk_Cartesian … (first … result_carry) (second … result_carry :: ac_flag :: ov_flag :: Empty Bool) 87  false ⇒ ? 88 ] 89  false ⇒ ? 90 ]. 91 80 92 81 93 ndefinition add_8_with_carry ≝ add_n_with_carry eight. 
Deliverables/D4.1/Matita/Assembly.ma
r271 r272 74 74 [ ADDR11 w ⇒ λ_. 75 75 let 〈v1,v2〉 ≝ split ? (S (S (S (S (S (S (S (S Z)))))))) (S (S (S Z))) w in 76 [ (v1 @ [[true; false; false; false; true]]) ; v2 ]76 [ (v1 @@ [[true; false; false; false; true]]) ; v2 ] 77 77  _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr) 78 78  ADD addr1 addr2 ⇒ 
Deliverables/D4.1/Matita/Vector.ma
r269 r272 237 237 ]. 238 238 239 interpretation "Vector append" 'append v1 v2 = (append ??? v1 v2). 239 notation "hvbox(l break @@ r)" 240 right associative with precedence 47 241 for @{ 'vappend $l $r }. 242 243 interpretation "Vector append" 'vappend v1 v2 = (append ??? v1 v2). 240 244 241 245 nlet rec scan_left (A: Type[0]) (B: Type[0]) (n: Nat)
Note: See TracChangeset
for help on using the changeset viewer.