Ignore:
Timestamp:
Dec 13, 2010, 5:00:02 PM (9 years ago)
Author:
mulligan
Message:

Using bitvectortries for a dictionary doesn't work even if we hypothesise conversion functions from bitvectors to string, and back again. Many changes, including most of the assembly function implemented.

File:
1 edited

Legend:

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

    r374 r410  
    77
    88include "Vector.ma".
     9include "String.ma".
    910
    1011(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
     
    217218        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218219    ].
     220   
     221naxiom bitvector_of_string:
     222  ∀n: Nat.
     223  ∀s: String.
     224    BitVector n.
     225   
     226naxiom string_of_bitvector:
     227  ∀n: Nat.
     228  ∀b: BitVector n.
     229    String.
Note: See TracChangeset for help on using the changeset viewer.