| 1 | include "basics/types.ma". |
|---|
| 2 | |
|---|
| 3 | include "utilities/adt/set_adt.ma". |
|---|
| 4 | include "utilities/adt/table_adt.ma". |
|---|
| 5 | |
|---|
| 6 | axiom set_table: Type[0] → Type[0] → Type[0]. |
|---|
| 7 | |
|---|
| 8 | axiom set_tbl_empty: ∀key_type, a. set_table key_type a. |
|---|
| 9 | axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option (set a). |
|---|
| 10 | axiom set_tbl_add: ∀key_type, a. key_type → set a |
|---|
| 11 | → set_table key_type (set a) → set_table key_type (set a). |
|---|
| 12 | axiom 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). |
|---|
| 14 | axiom set_tbl_mkedge: ∀key_type, a. key_type → a → set_table key_type (set a) → |
|---|
| 15 | set_table key_type (set a). |
|---|
| 16 | axiom set_tbl_rmedge: ∀key_type, a. key_type → a → set_table key_type (set a) → |
|---|
| 17 | set_table key_type (set a). |
|---|
| 18 | axiom set_tbl_iter: ∀key_type, a. (key_type → a → a) → |
|---|
| 19 | set_table key_type (set a) → set_table key_type (set a). |
|---|
| 20 | axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b) |
|---|
| 21 | → set_table key_type a -> b -> b. |
|---|
| 22 | axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) → |
|---|
| 23 | ((key_type × a) → bool) → option (key_type × a). |
|---|
| 24 | |
|---|
| 25 | |
|---|
| 26 | axiom set_tbl_homo_mkbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type). |
|---|
| 27 | axiom set_tbl_homo_rmbiedge: ∀key_type. key_type → key_type → set_table key_type (set key_type) → set_table key_type (set key_type). |
|---|
| 28 | axiom set_tbl_homo_reverse: ∀key_type. set_table key_type (set key_type) → set_table key_type (set key_type). |
|---|
| 29 | axiom set_tbl_homo_restrict: ∀key_type. (key_type → bool) → set_table key_type (set key_type) → set_table key_type (set key_type). |
|---|
