Ignore:
Timestamp:
Sep 14, 2011, 5:03:17 PM (9 years ago)
Author:
mulligan
Message:

more added on interference graphs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/adt/set_table_adt.ma

    r1210 r1212  
    44include "utilities/adt/table_adt.ma".
    55include "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 TracChangeset for help on using the changeset viewer.