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

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

File:
1 edited

Legend:

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

    r232 r234  
     1include "List.ma".
    12include "Vector.ma".
    23include "Nat.ma".
     
    3132  λc: BitVector n.
    3233    zip Bool Bool Bool n exclusive_disjunction b c.
     34   
     35ndefinition complement ≝
     36  λn: Nat.
     37  λb: BitVector n.
     38    map Bool Bool n (negation) b.
    3339
    34 nlet rec pad (n: Nat) (m: Nat) (b: BitVector n) (p: less_than_or_equal_p n m): (BitVector (n + m)) ≝
    35   match m with
    36     [ Z ⇒ ?
    37     | S o ⇒ ?
    38     ].
    39    
    40     //.
    41 nqed.
     40ndefinition divide_with_remainder ≝
     41  λm, n: Nat.
     42    mk_Cartesian Nat Nat (m ÷ n) (modulus m n).
    4243
    43 ncheck pad.
    44        
     44nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝
     45  let div_rem ≝ divide_with_remainder n (S (S Z)) in
     46  let div ≝ first Nat Nat div_rem in
     47  let rem ≝ second Nat Nat div_rem in
     48    Empty Nat.
Note: See TracChangeset for help on using the changeset viewer.