source: Deliverables/D4.1/Matita/Compare.ma @ 418

Last change on this file since 418 was 410, checked in by mulligan, 10 years ago

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 size: 109 bytes
Line 
1include "Universes.ma".
2
3ninductive Compare: Type[0] ≝
4  Equal: Compare
5| Less: Compare
6| Greater: Compare.
Note: See TracBrowser for help on using the repository browser.