Changeset 724 for src/ASM/Arithmetic.ma
 Timestamp:
 Mar 30, 2011, 2:03:05 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r712 r724 114 114 λb: BitVector n. 115 115 \fst (sub_with_borrows n b (zero n) true). 116 116 117 let rec bitvector_of_nat_aux (n,m:nat) (v:BitVector n) on m : BitVector n ≝ 118 match m with 119 [ O ⇒ v 120  S m' ⇒ bitvector_of_nat_aux n m' (increment n v) 121 ]. 122 123 definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝ 124 λn,m. bitvector_of_nat_aux n m (zero n). 125 126 let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝ 127 match v with 128 [ VEmpty ⇒ m 129  VCons n' hd tl ⇒ nat_of_bitvector_aux n' (if hd then 2*m +1 else 2*m) tl 130 ]. 131 132 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ 133 λn,v. nat_of_bitvector_aux n O v. 134 117 135 definition two_complement_negation ≝ 118 136 λn: nat.
Note: See TracChangeset
for help on using the changeset viewer.