Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/utilities/RegisterSet.ma

    r1075 r1197  
    1111  rs_exists: Register → rs_set → bool;
    1212  rs_union: rs_set → rs_set → rs_set;
     13  rs_subset: rs_set → rs_set → bool;
    1314  rs_to_list: rs_set → list Register;
    1415  rs_from_list: list Register → rs_set
     
    4546  λs: list Register.
    4647    nub_by ? eq_Register (r @ s).
     48
     49definition rs_list_set_subset ≝
     50  λr: list Register.
     51  λs: list Register.
     52    forall … (λx. member … eq_Register x s) r.
    4753 
    4854definition rs_list_set_from_list ≝
     
    5561                  rs_list_set_insert rs_list_set_exists
    5662                  rs_list_set_union
     63                  rs_list_set_subset
    5764                  (λx. x) rs_list_set_from_list.
Note: See TracChangeset for help on using the changeset viewer.