module Set: Equality_sig.Set
with type element = elt and type equality = t
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