`Predicate.S`

`val empty : t`

The empty set.

`val full : t`

The set of all elements (of type `elm`

).

`val is_empty : t -> bool`

Test whether a set is empty or not.

`val is_full : t -> bool`

Test whether a set contains the whole type or not.

`add x s`

returns a set containing all elements of `s`

, plus `x`

. If `x`

was already in `s`

, then `s`

is returned unchanged.

`remove x s`

returns a set containing all elements of `s`

, except `x`

. If `x`

was not in `s`

, then `s`

is returned unchanged.

`equal s1 s2`

tests whether the sets `s1`

and `s2`

are equal, that is, contain equal elements.

Gives a finite representation of the predicate: if the boolean is false, then the predicate is given in extension. if it is true, then the complement is given

`val is_finite : t -> bool`

`true`

if the predicate can be given as a finite set (if `elt`

is a finite type, we can have `is_finite x = false`

yet `x`

is finite, but we don't know how to list its elements)