module Make (E : Index.EQUATION) : Index.UNIT_IDX with module E = E
type
module E: Index_intf.EQUATION
Module that describes indexed equations
type E.rhs
Right hand side of equation
val empty : unit -> t
val is_empty : t -> bool
val add : t -> E.t -> t
Index the given (in)equation
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
Number of indexed (in)equations
val iter : t -> (Index_intf.term -> E.t -> unit) -> unit
Iterate on indexed equations
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
retrieve ~sign (idx,si) (t,st) acc iterates on
(in)equations l ?= r of given sign and substitutions subst,
such that subst(l, si) = t.
It therefore finds generalizations of the query term.
val to_dot : t CCFormat.printer
print the index in the DOT format