Ignore:
Timestamp:
Dec 1, 2010, 6:40:15 PM (9 years ago)
Author:
mulligan
Message:
  • pc was initialized to 7 in place of sp
  • bitvector_of_nat was totally bugged: fixed
File:
1 edited

Legend:

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

    r351 r353  
    166166    vector_of_list Bool l.
    167167
    168 nlet rec bitvector_of_nat_aux (n: Nat) on n ≝
    169   let divrem ≝ divide_with_remainder n (S (S Z)) in
    170   let div ≝ first Nat Nat divrem in
    171   let rem ≝ second Nat Nat divrem in
    172     match div with
    173       [ Z ⇒
    174         match rem with
    175           [ Z ⇒ Empty Bool
    176           | S r ⇒ ? (true :: (bitvector_of_nat_aux Z))
    177           ]
    178       | S d ⇒
    179         match rem with
    180           [ Z ⇒ ? (false :: (bitvector_of_nat_aux (S d)))
    181           | S r ⇒ ? (true :: (bitvector_of_nat_aux (S d)))
    182           ]
    183       ].
    184       //.
    185 nqed.
     168nlet rec bitvector_of_nat_aux (n: Nat) (bound: Nat) on bound ≝
     169 match bound with
     170  [ Z ⇒ Empty Bool (* IT WILL NOT HAPPEN *)
     171  | S bound ⇒
     172    let divrem ≝ divide_with_remainder n (S (S Z)) in
     173    let div ≝ first Nat Nat divrem in
     174    let rem ≝ second Nat Nat divrem in
     175      match div with
     176        [ Z ⇒
     177          match rem with
     178            [ Z ⇒ Empty Bool
     179            | S r ⇒ true :: (bitvector_of_nat_aux Z bound)
     180            ]
     181        | S d ⇒
     182          match rem with
     183            [ Z ⇒ false :: (bitvector_of_nat_aux (S d) bound)
     184            | S r ⇒ true :: (bitvector_of_nat_aux (S d) bound)
     185            ]
     186        ]].
    186187
    187188ndefinition eq_bv ≝
     
    196197
    197198nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝
    198   let biglist ≝ reverse ? (bitvector_of_nat_aux m) in
     199  let biglist ≝ reverse ? (bitvector_of_nat_aux m m) in
    199200  let size ≝ length ? biglist in
    200201  let bitvector ≝ bitvector_of_list biglist in
Note: See TracChangeset for help on using the changeset viewer.