Module type 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.
val add : elt -> t -> t
add x s
returns a set containing all elements ofs
, plusx
. Ifx
was already ins
, thens
is returned unchanged.
val remove : elt -> t -> t
remove x s
returns a set containing all elements ofs
, exceptx
. Ifx
was not ins
, thens
is returned unchanged.
val equal : t -> t -> bool
equal s1 s2
tests whether the setss1
ands2
are equal, that is, contain equal elements.
val elements : t -> bool * elt list
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 (ifelt
is a finite type, we can haveis_finite x = false
yetx
is finite, but we don't know how to list its elements)