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