module type Set = sig
.. end
Sets of equalities.
type
element
The type of the equality elements.
type
equality
The type of the equalities.
include Datatype.S
The set operators are redefined so that equalities involving a same term
are joined: ∀ e₁, e₂ ∈ Set, e₁ ≠ e₂ ⇔ e₁ ∩ e₂ = ∅
val empty : t
val is_empty : t -> bool
val add : equality -> t -> t
val singleton : equality -> t
val union : t -> t -> t
val inter : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (equality -> unit) -> t -> unit
val fold : (equality -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (equality -> bool) -> t -> bool
val exists : (equality -> bool) -> t -> bool
val elements : t -> equality list
val choose : t -> equality
val remove : element -> t -> t
remove elt set
remove any occurrence of elt
in set
.
val unite : element -> element -> t -> t
unite a b map
unites a
and b
in map
.
val find : element -> t -> equality
find elt set
return the (single) equality involving elt
that belongs to set
, or raise Not_found if no such equality exists.
val find_option : element -> t -> equality option
Same as find
, but return None in the last case.
val mem : equality -> t -> bool
mem equality set
= true iff ∃ eq ∈ set, equality ⊆ eq
val contains : element -> t -> bool
contains elt set
= true iff elt
belongs to an equality of set
.
val diff : t -> t -> t
val subst : (element -> element option) -> t -> t
val deep_fold : (equality -> element -> 'a -> 'a) ->
t -> 'a -> 'a
val terms : t -> element list
terms set
return the list of elements of equality of set
.
val cardinal : t -> int