Changeset 2177
 Timestamp:
 Jul 12, 2012, 2:56:50 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2154 r2177 364 364 ]. 365 365 366 definition short_multiplication : ∀n:nat. BitVector n → BitVector n → BitVector n ≝ 367 λn,x,y. (\snd (vsplit ??? (multiplication ? x y))). 368 366 369 (* Division: 001...000 divided by 000...010 367 370 Shift the divisor as far left as possible, 
src/Clight/Csem.ma
r2176 r2177 197 197 [ Vint sz1 n1 ⇒ match v2 with 198 198 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 199 (λn1. Some ? (Vint sz2 ( \snd (vsplit ??? (multiplication ? n1 n2))))) (None ?)199 (λn1. Some ? (Vint sz2 (short_multiplication ? n1 n2))) (None ?) 200 200  _ ⇒ None ? ] 201 201  _ ⇒ None ? ] 
src/common/FrontEndOps.ma
r2176 r2177 244 244 [ Vint sz1 n1 ⇒ match v2 with 245 245 [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 246 (λn1. Some ? (Vint ? ( \snd (vsplit … (multiplication ? n1 n2)))))246 (λn1. Some ? (Vint ? (short_multiplication ? n1 n2))) 247 247 (None ?) 248 248  _ ⇒ None ? ]
Note: See TracChangeset
for help on using the changeset viewer.