Changeset 782 for src/utilities
- Timestamp:
- Apr 28, 2011, 5:36:33 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/RegisterSet.ma
r778 r782 10 10 rs_insert: register → rs_set → rs_set; 11 11 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 13 15 }. 14 16 … … 44 46 nub_by ? (eq_identifier ?) (r @ s). 45 47 48 definition rs_list_set_from_list ≝ 49 λr: list register. 50 nub_by ? (eq_identifier ?) r. 51 46 52 definition register_list_set: register_set ≝ 47 53 mk_register_set (list register) rs_list_set_empty 48 54 rs_list_set_singleton rs_list_set_fold 49 55 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.