Module Gospelstdlib.Set

Gospel declaration:
    type 'a t = 'a set 

An alias for 'a set.

Gospel declaration:
    function compare (s s': 'a t) : integer 

A comparison function over sets.

Gospel declaration:
    function empty : 'a t 

empty is ∅.

Gospel declaration:
    predicate is_empty (s: 'a t) 

is_empty s is s = ∅.

Gospel declaration:
    predicate mem (x: 'a) (s: 'a t) 

mem x s is x ∈ s.

Gospel declaration:
    function add (x: 'a) (s: 'a t) : 'a t 

add x s is s ∪ {x}.

Gospel declaration:
    function singleton (x: 'a) : 'a t 

singleton x is {x}.

Gospel declaration:
    function remove (x: 'a) (s: 'a t) : 'a t 

remove x s is s ∖ {x}.

Gospel declaration:
    function union (s s': 'a t) : 'a t 

union s s' is s ∪ s'.

Gospel declaration:
    function inter (s s': 'a t) : 'a t 

inter s s' is s ∩ s'.

Gospel declaration:
    predicate disjoint (s s': 'a t) 

disjoint s s' is s ∩ s' = ∅.

Gospel declaration:
    function diff (s s': 'a t) : 'a t 

diff s s' is s ∖ s'.

Gospel declaration:
    predicate subset (s s': 'a t) 

subset s s' is s ⊂ s'.

Gospel declaration:
    function cardinal (s: 'a t) : integer 

cardinal s is the number of elements in s.

Gospel declaration:
    function choose (s: 'a t) : integer 

choose s is an arbitrary element of s.

Gospel declaration:
    function choose_opt: 'a t -> 'a option 

choose_opt s is an arbitrary element of s or None if s is empty.

Gospel declaration:
    function map (f: 'a -> 'b) (s: 'a t) : 'b t 

map f s is a fresh set which elements are f x1 ... f xN, where x1 ... xN are the elements of s.

Gospel declaration:
    function fold (f: 'a -> 'b -> 'b) (s: 'a t) (a: 'b) : 'b 

fold f s a is (f xN ... (f x2 (f x1 a))...), where x1 ... xN are the elements of s.

Gospel declaration:
    predicate for_all (f: 'a -> bool) (s: 'a t) 

for_all f s holds iff f x is true for all elements in s.

Gospel declaration:
    predicate _exists (f: 'a -> bool) (s: 'a t) 

_exists f s holds iff f x is true for at least one element in s.

Gospel declaration:
    function filter (f: 'a -> bool) (s: 'a t) : 'a t 

filter f s is the set of all elements in s that satisfy f.

Gospel declaration:
    function filter_map (f: 'a -> 'a option) (s: 'a t) : 'a t 

filter_map f s is the set of all v such that f x = Some v for some element x of s.

Gospel declaration:
    function partition (f: 'a -> bool) (s: 'a t) : ('a t * 'a t) 

partition f s is the pair of sets (s1, s2), where s1 is the set of all the elements of s that satisfy the predicate f, and s2 is the set of all the elements of s that do not satisfy f.

Gospel declaration:
    function to_list (s: 'a t) : 'a list 

Gospel declaration:
    function of_list (l: 'a list) : 'a t 

Gospel declaration:
    function to_seq (s: 'a t) : 'a Sequence.t 

Gospel declaration:
    function of_seq (s: 'a Sequence.t) : 'a t