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