Changeset 724 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Mar 30, 2011, 2:03:05 PM (9 years ago)
Author:
campbell
Message:

More tractable version of bitvector_of_nat / nat_of_bitvector.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r712 r724  
    114114  λb: BitVector n.
    115115    \fst (sub_with_borrows n b (zero n) true).
    116    
     116
     117let 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
     123definition bitvector_of_nat : ∀n:nat. nat → BitVector n ≝
     124  λn,m. bitvector_of_nat_aux n m (zero n).
     125
     126let rec nat_of_bitvector_aux (n,m:nat) (v:BitVector n) on v : nat ≝
     127match 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
     132definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝
     133  λn,v. nat_of_bitvector_aux n O v.
     134
    117135definition two_complement_negation ≝
    118136  λn: nat.
Note: See TracChangeset for help on using the changeset viewer.