Ignore:
Timestamp:
Sep 15, 2011, 4:56:30 PM (9 years ago)
Author:
mulligan
Message:

a lot added to interference graph calculation

File:
1 edited

Legend:

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

    r1212 r1218  
    77axiom set_table: Type[0] → Type[0] → Type[0].
    88
    9 axiom set_tbl_find: ∀key_type, a. key_type → set_table key_type (set a) → option a.
     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).
    1011axiom set_tbl_add: ∀key_type, a. key_type → set a
    1112                     → set_table key_type (set a) → set_table key_type (set a).
     
    1920                      set_table key_type (set a) → set_table key_type (set a).
    2021axiom set_tbl_fold: ∀key_type, a, b: Type[0]. (key_type → a → b → b)
    21                       → set_table key_type (set a) -> b -> b.
     22                      → set_table key_type a -> b -> b.
    2223axiom set_tbl_pick: ∀key_type, a. set_table key_type (set a) →
    2324                      (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 TracChangeset for help on using the changeset viewer.