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

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

more added on interference graphs

File size: 1.3 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_find: ∀key_type, a. key_type → set_table key_type (set a) → option a.
10axiom set_tbl_add: ∀key_type, a. key_type → set a
11                     → set_table key_type (set a) → set_table key_type (set a).
12axiom set_tbl_update: ∀key_type, a. key_type → (set a → set a) → set_table key_type (set a)
13                     → set_table key_type (set a).
14axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
15                         set_table key_type (set a).
16axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) →
17                         set_table key_type (set a).
18axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) →
19                      set_table key_type (set a) → set_table key_type (set a).
20axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
21                      → set_table key_type (set a) -> b -> b.
22axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
23                      (key_type → a → bool) → option (key_type × a).
Note: See TracBrowser for help on using the repository browser.