source: src/utilities/adt/set_table_adt.ma @ 1218

Last change on this file since 1218 was 1218, checked in by mulligan, 9 years ago

a lot added to interference graph calculation

File size: 1.8 KB
Line 
1include "basics/types.ma".
2
3include "utilities/adt/set_adt.ma".
4include "utilities/adt/table_adt.ma".
5include "utilities/adt/ordering.ma".
6
7axiom set_table: Type[0] → Type[0] → Type[0].
8
9axiom set_tbl_empty: ∀key_type, a. set_table key_type a.
10axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set a).
11axiom set_tbl_add: ∀key_type, a. key_type → set a
12                     → set_table key_type (set a) → set_table key_type (set a).
13axiom set_tbl_update: ∀key_type, a. key_type → (set a → set a) → set_table key_type (set a)
14                     → set_table key_type (set a).
15axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
16                         set_table key_type (set a).
17axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
18                         set_table key_type (set a).
19axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) →
20                      set_table key_type (set a) → set_table key_type (set a).
21axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
22                      → set_table key_type a -> b -> b.
23axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
24                      (key_type → a → bool) → option (key_type × a).
25
26
27axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
28axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
29axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type).
30axiom set_tbl_homo_restrict: ∀key_type. (key_type → bool) → set_table key_type (set key_type) → set_table key_type (set key_type).
Note: See TracBrowser for help on using the repository browser.