Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/bitVectorZ.ml

    r2717 r2773  
    2020
    2121open Z
     22
     23open Setoids
     24
     25open Monad
     26
     27open Option
    2228
    2329open Extranat
     
    9096| Z.Pos p ->
    9197  let bits = bits_of_pos p in
    92   Vector.reverse0 n
     98  Vector.reverse n
    9399    (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
    94100| Z.Neg p ->
     
    96102   | Positive.One -> BitVector.maximum n
    97103   | Positive.P1 x ->
    98      let bits = bits_of_pos (Positive.pred0 p) in
     104     let bits = bits_of_pos (Positive.pred p) in
    99105     let pz =
    100        Vector.reverse0 n
     106       Vector.reverse n
    101107         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
    102108     in
    103109     BitVector.negation_bv n pz
    104110   | Positive.P0 x ->
    105      let bits = bits_of_pos (Positive.pred0 p) in
     111     let bits = bits_of_pos (Positive.pred p) in
    106112     let pz =
    107        Vector.reverse0 n
     113       Vector.reverse n
    108114         (zeroext_reversed (List.length bits) n (Vector.vector_of_list bits))
    109115     in
Note: See TracChangeset for help on using the changeset viewer.