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

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

changes

File size: 1.8 KB
Line 
1include "basics/types.ma".
2
3include "utilities/adt/set_adt.ma".
4include "utilities/adt/table_adt.ma".
5
6axiom set_table: Type[0] → Type[0] → Type[0].
7
8axiom set_tbl_empty: ∀key_type, a. set_table key_type a.
9axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set 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 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).
24
25
26axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
27axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type).
28axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type).
29axiom 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.