sig
type t
module E :
sig
type t = Logtk.Term.t * Logtk.Term.t * bool * C.t
type rhs = Logtk.Term.t
val compare : t -> t -> int
val extract : t -> Logtk.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 -> (Logtk.Index_intf.term -> E.t -> unit) -> unit
val retrieve :
?subst:Logtk.Index_intf.subst ->
sign:bool ->
t Logtk.Scoped.t ->
Logtk.Index_intf.term Logtk.Scoped.t ->
(Logtk.Index_intf.term * rhs * E.t * Logtk.Index_intf.subst) Sequence.t
val to_dot : t CCFormat.printer
end