Changeset 235
 Timestamp:
 Nov 12, 2010, 2:43:02 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r234 r235 1 include "Vector.ma". 1 2 include "List.ma". 2 include "Vector.ma".3 3 include "Nat.ma". 4 4 include "Bool.ma". … … 42 42 mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 43 43 44 nlet rec bitvector_of_nat_aux (n: Nat) : List Nat≝44 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝ 45 45 let div_rem ≝ divide_with_remainder n (S (S Z)) in 46 46 let div ≝ first Nat Nat div_rem in 47 47 let rem ≝ second Nat Nat div_rem in 48 Empty Nat. 48 match div with 49 [ Z ⇒ 50 match rem with 51 [ Z ⇒ Empty Bool 52  S r ⇒ True :: (bitvector_of_nat_aux Z) 53 ] 54  S d ⇒ 55 match rem with 56 [ Z ⇒ False :: (bitvector_of_nat_aux (S d)) 57  S r ⇒ True :: (bitvector_of_nat_aux (S d)) 58 ] 59 ].
Note: See TracChangeset
for help on using the changeset viewer.