sig
type t
module E :
sig
type t =
Libzipperposition.FOTerm.t * Libzipperposition.FOTerm.t * bool *
C.t
type rhs = Libzipperposition.FOTerm.t
val compare : t -> t -> int
val extract : t -> Libzipperposition.Index_intf.term * rhs * bool
val priority : t -> int
end
type rhs = E.rhs
val empty : unit -> t
val is_empty : t -> bool
val add : t -> E.t -> t
val add_seq : t -> E.t Sequence.t -> t
val add_list : t -> E.t list -> t
val remove : t -> E.t -> t
val remove_seq : t -> E.t Sequence.t -> t
val size : t -> int
val iter : t -> (Libzipperposition.Index_intf.term -> E.t -> unit) -> unit
val retrieve :
?subst:Libzipperposition.Index_intf.subst ->
sign:bool ->
t Libzipperposition.Scoped.t ->
Libzipperposition.Index_intf.term Libzipperposition.Scoped.t ->
(Libzipperposition.Index_intf.term * rhs * E.t *
Libzipperposition.Index_intf.subst)
Sequence.t
val to_dot : t CCFormat.printer
end