Module Predicate.Make
The Make functor constructs an implementation for any OrderedType.
Parameters
Signature
type elt= Ord.tThe type of the elements in the set.
val empty : tThe empty set.
val full : tThe set of all elements (of type
elm).
val is_empty : t -> boolTest whether a set is empty or not.
val is_full : t -> boolTest whether a set contains the whole type or not.
val add : elt -> t -> tadd x sreturns a set containing all elements ofs, plusx. Ifxwas already ins, thensis returned unchanged.
val remove : elt -> t -> tremove x sreturns a set containing all elements ofs, exceptx. Ifxwas not ins, thensis returned unchanged.
val equal : t -> t -> boolequal s1 s2tests whether the setss1ands2are equal, that is, contain equal elements.
val elements : t -> bool * elt listGives 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 -> booltrueif the predicate can be given as a finite set (ifeltis a finite type, we can haveis_finite x = falseyetxis finite, but we don't know how to list its elements)