Changeset 746 for src/ERTL/Uses.ma


Ignore:
Timestamp:
Apr 8, 2011, 11:51:38 AM (10 years ago)
Author:
mulligan
Message:

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Uses.ma

    r745 r746  
    99    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
    1010      insert ? 16 register l uses.
    11      
    12 definition word_of_register: Register → Word ≝
    13   λregister.
    14     bitvector_of_nat ? (nat_of_register register).
    1511     
    1612definition examine_statement ≝
Note: See TracChangeset for help on using the changeset viewer.