Changeset 2773 for extracted/bitVectorZ.ml
 Timestamp:
 Mar 4, 2013, 10:03:33 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

extracted/bitVectorZ.ml
r2717 r2773 20 20 21 21 open Z 22 23 open Setoids 24 25 open Monad 26 27 open Option 22 28 23 29 open Extranat … … 90 96  Z.Pos p > 91 97 let bits = bits_of_pos p in 92 Vector.reverse 0n98 Vector.reverse n 93 99 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) 94 100  Z.Neg p > … … 96 102  Positive.One > BitVector.maximum n 97 103  Positive.P1 x > 98 let bits = bits_of_pos (Positive.pred 0p) in104 let bits = bits_of_pos (Positive.pred p) in 99 105 let pz = 100 Vector.reverse 0n106 Vector.reverse n 101 107 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) 102 108 in 103 109 BitVector.negation_bv n pz 104 110  Positive.P0 x > 105 let bits = bits_of_pos (Positive.pred 0p) in111 let bits = bits_of_pos (Positive.pred p) in 106 112 let pz = 107 Vector.reverse 0n113 Vector.reverse n 108 114 (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits)) 109 115 in
Note: See TracChangeset
for help on using the changeset viewer.