Changeset 782 for src/utilities


Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (10 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/utilities/RegisterSet.ma

    r778 r782  
    1010  rs_insert: register → rs_set → rs_set;
    1111  rs_exists: register → rs_set → bool;
    12   rs_union: rs_set → rs_set → rs_set
     12  rs_union: rs_set → rs_set → rs_set;
     13  rs_to_list: rs_set → list register;
     14  rs_from_list: list register → rs_set
    1315}.
    1416
    … …  
    4446    nub_by ? (eq_identifier ?) (r @ s).
    4547 
     48definition rs_list_set_from_list ≝
     49  λr: list register.
     50    nub_by ? (eq_identifier ?) r.
     51 
    4652definition register_list_set: register_set ≝
    4753  mk_register_set (list register) rs_list_set_empty
    4854                  rs_list_set_singleton rs_list_set_fold
    4955                  rs_list_set_insert rs_list_set_exists
    50                   rs_list_set_union.
     56                  rs_list_set_union
     57                  (λx. x) rs_list_set_from_list.
Note: See TracChangeset for help on using the changeset viewer.