# Module `Id.Pred`

Predicates over identifiers.

`type elt = t`

The type of the elements in the set.

`type t`

The type of sets.

`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 mem : elt -> t -> bool`

`mem x s` tests whether `x` belongs to the set `s`.

`val singleton : elt -> t`

`singleton x` returns the one-element set containing only `x`.

`val add : elt -> t -> t`

`add x s` returns a set containing all elements of `s`, plus `x`. If `x` was already in `s`, then `s` is returned unchanged.

`val remove : elt -> t -> t`

`remove x s` returns a set containing all elements of `s`, except `x`. If `x` was not in `s`, then `s` is returned unchanged.

`val union : t -> t -> t`

Set union.

`val inter : t -> t -> t`

Set intersection.

`val diff : t -> t -> t`

Set difference.

`val complement : t -> t`

Set complement.

`val equal : t -> t -> bool`

`equal s1 s2` tests whether the sets `s1` and `s2` are equal, that is, contain equal elements.

`val subset : t -> t -> bool`

`subset s1 s2` tests whether the set `s1` is a subset of the set `s2`.

`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 (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)