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/Nat.ma

    r363 r410  
    719719ndefinition two_hundred_and_forty ≝ two_hundred_and_twenty_four + sixteen.
    720720ndefinition two_hundred_and_fifty_six ≝
    721   one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.                                       
     721  one_hundred_and_twenty_eight + one_hundred_and_twenty_eight.
     722ndefinition sixty_five_thousand_five_hundred_and_thirty_six ≝
     723  two_hundred_and_fifty_six * two_hundred_and_fifty_six.
Note: See TracChangeset for help on using the changeset viewer.