Ignore:
Timestamp:
Mar 4, 2013, 10:03:33 AM (7 years ago)
Author:
sacerdot
Message:
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File:
1 edited

Legend:

Unmodified
Added
Removed
  • extracted/untrusted/set_adt.ml

    r2738 r2773  
    33let matitabool_of_bool b = if b then Bool.True else Bool.False
    44
    5 (** val set_empty : 'a1 set0 **)
     5(** val set_empty : 'a1 set **)
    66let set_empty = Pset.empty
    77
    88(** val set_member :
    9     ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set0 -> Bool.bool **)
     9    ('a1 -> 'a1 -> Bool.bool) -> 'a1 -> 'a1 set -> Bool.bool **)
    1010let set_member _ x s = matitabool_of_bool (Pset.mem x s)
    1111
    1212(** val set_equal :
    13     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
     13    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool **)
    1414let set_equal _ s1 s2 = matitabool_of_bool (Pset.equal s1 s2)
    1515
    16 (** val set_diff : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
     16(** val set_diff : 'a1 set -> 'a1 set -> 'a1 set **)
    1717let set_diff = Pset.diff
    1818
    19 (** val set_singleton : 'a1 -> 'a1 set0 **)
     19(** val set_singleton : 'a1 -> 'a1 set **)
    2020let set_singleton = Pset.singleton
    2121
    22 (** val set_from_list : 'a1 List.list -> 'a1 set0 **)
     22(** val set_from_list : 'a1 List.list -> 'a1 set **)
    2323let set_from_list the_list =
    2424  List.foldr Pset.add set_empty the_list
    2525
    2626(** val set_subset :
    27     ('a1 -> 'a1 -> Bool.bool) -> 'a1 set0 -> 'a1 set0 -> Bool.bool **)
     27    ('a1 -> 'a1 -> Bool.bool) -> 'a1 set -> 'a1 set -> Bool.bool **)
    2828let set_subset _ s1 s2 = matitabool_of_bool (Pset.subset s1 s2)
    2929
    30 (** val set_union : 'a1 set0 -> 'a1 set0 -> 'a1 set0 **)
     30(** val set_union : 'a1 set -> 'a1 set -> 'a1 set **)
    3131let set_union = Pset.union
Note: See TracChangeset for help on using the changeset viewer.