 Timestamp:
 Nov 2, 2011, 6:58:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1426 r1485 19 19 let 〈lower_bits, carries〉 ≝ r in 20 20 let last_carry ≝ match carries with [ VEmpty ⇒ init_carry  VCons _ cy _ ⇒ cy ] in 21 let bit ≝ exclusive_disjunction (exclusive_disjunction b c) last_carry in 22 let carry ≝ carry_of b c last_carry in 21 (* Next ifthenelse just to avoid a quadratic blowup of the whd of an application 22 of add_with_carries *) 23 if last_carry then 24 let bit ≝ exclusive_disjunction (exclusive_disjunction b c) true in 25 let carry ≝ carry_of b c true in 23 26 〈bit:::lower_bits, carry:::carries〉 27 else 28 let bit ≝ exclusive_disjunction (exclusive_disjunction b c) false in 29 let carry ≝ carry_of b c false in 30 〈bit:::lower_bits, carry:::carries〉 24 31 ) 25 32 〈[[ ]], [[ ]]〉 n x y.
Note: See TracChangeset
for help on using the changeset viewer.