Changeset 2733 for extracted/set_adt.mli


Ignore:
Timestamp:
Feb 25, 2013, 11:04:57 PM (8 years ago)
Author:
sacerdot
Message:

All axioms in set_adt implemented by hand.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/set_adt.mli

    r2730 r2733  
    33val set_empty : 'a1 set
    44
    5 val set_size : 'a1 set -> Nat.nat
    6 
    7 val set_to_list : 'a1 set -> 'a1 List.list
    8 
    9 val set_insert : 'a1 -> 'a1 set -> 'a1 set
    10 
    11 val set_remove : 'a1 -> 'a1 set -> 'a1 set
    12 
    135val set_member : ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set -> Bool.bool
    14 
    15 val set_forall : ('a1 -> Bool.bool) -> 'a1 set -> Bool.bool
    16 
    17 val set_exists : ('a1 -> Bool.bool) -> 'a1 set -> Bool.bool
    18 
    19 val set_filter : ('a1 -> Bool.bool) -> 'a1 set -> 'a1 set
    20 
    21 val set_map : ('a1 -> 'a2) -> 'a1 set -> 'a2 set
    22 
    23 val set_fold : ('a1 -> 'a2 -> 'a2) -> 'a1 set -> 'a2 -> 'a2
    246
    257val set_equal :
     
    2810val set_diff : 'a1 set -> 'a1 set -> 'a1 set
    2911
    30 val set_is_empty : 'a1 set -> Bool.bool
    31 
    3212val set_singleton : 'a1 -> 'a1 set
    3313
    3414val set_from_list : 'a1 List.list -> 'a1 set
    3515
    36 val set_split :
    37   ('a1 -> Bool.bool) -> 'a1 set -> ('a1 set, 'a1 set) Types.prod
    38 
    3916val set_subset :
    4017  ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
    4118
    42 val set_subseteq :
    43   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool
    44 
    4519val set_union : 'a1 set -> 'a1 set -> 'a1 set
    46 
    47 val set_intersection :
    48   ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> 'a1 set
    49 
Note: See TracChangeset for help on using the changeset viewer.