sig
  type t
  type elt = C.WithPos.t
  module Leaf :
    sig
      type t
      type elt = elt
      val empty : t
      val add : t -> Logtk.Index_intf.term -> elt -> t
      val remove : t -> Logtk.Index_intf.term -> elt -> t
      val is_empty : t -> bool
      val iter : t -> (Logtk.Index_intf.term -> elt -> unit) -> unit
      val fold : t -> 'a -> ('a -> Logtk.Index_intf.term -> elt -> 'a) -> 'a
      val size : t -> int
      val fold_unify :
        ?subst:Logtk.Unif_subst.t ->
        t Logtk.Scoped.t ->
        Logtk.Index_intf.term Logtk.Scoped.t ->
        (Logtk.Index_intf.term * elt * Logtk.Unif_subst.t) Sequence.t
      val fold_match :
        ?subst:Logtk.Index_intf.subst ->
        t Logtk.Scoped.t ->
        Logtk.Index_intf.term Logtk.Scoped.t ->
        (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst) Sequence.t
      val fold_matched :
        ?subst:Logtk.Index_intf.subst ->
        t Logtk.Scoped.t ->
        Logtk.Index_intf.term Logtk.Scoped.t ->
        (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst) Sequence.t
    end
  val name : string
  val empty : unit -> t
  val is_empty : t -> bool
  val size : t -> int
  val add : t -> Logtk.Index_intf.term -> elt -> t
  val add_seq : t -> (Logtk.Index_intf.term * elt) Sequence.t -> t
  val add_list : t -> (Logtk.Index_intf.term * elt) list -> t
  val remove : t -> Logtk.Index_intf.term -> elt -> t
  val remove_seq : t -> (Logtk.Index_intf.term * elt) Sequence.t -> t
  val remove_list : t -> (Logtk.Index_intf.term * elt) list -> t
  val iter : t -> (Logtk.Index_intf.term -> elt -> unit) -> unit
  val fold : t -> ('a -> Logtk.Index_intf.term -> elt -> 'a) -> 'a -> 'a
  val retrieve_unifiables :
    ?subst:Logtk.Unif_subst.t ->
    t Logtk.Scoped.t ->
    Logtk.Index_intf.term Logtk.Scoped.t ->
    (Logtk.Index_intf.term * elt * Logtk.Unif_subst.t) Sequence.t
  val retrieve_generalizations :
    ?subst:Logtk.Index_intf.subst ->
    t Logtk.Scoped.t ->
    Logtk.Index_intf.term Logtk.Scoped.t ->
    (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst) Sequence.t
  val retrieve_specializations :
    ?subst:Logtk.Index_intf.subst ->
    t Logtk.Scoped.t ->
    Logtk.Index_intf.term Logtk.Scoped.t ->
    (Logtk.Index_intf.term * elt * Logtk.Index_intf.subst) Sequence.t
  val to_dot : elt CCFormat.printer -> t CCFormat.printer
end