Ignore:
Timestamp:
Nov 12, 2010, 2:43:02 PM (9 years ago)
Author:
mulligan
Message:

More work on bitvectors.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r234 r235  
     1include "Vector.ma".
    12include "List.ma".
    2 include "Vector.ma".
    33include "Nat.ma".
    44include "Bool.ma".
     
    4242    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
    4343
    44 nlet rec bitvector_of_nat_aux (n: Nat): List Nat
     44nlet rec bitvector_of_nat_aux (n: Nat) on n
    4545  let div_rem ≝ divide_with_remainder n (S (S Z)) in
    4646  let div ≝ first Nat Nat div_rem in
    4747  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.