Module type Index_intf.UNIT_IDX
type rhs
= E.rhs
Right hand side of equation
val add_seq : t -> E.t Iter.t -> t
val add_list : t -> E.t list -> t
val remove : t -> E.t -> t
val remove_seq : t -> E.t Iter.t -> t
val size : t -> int
Number of indexed (in)equations
val retrieve : ?subst:subst -> sign:bool -> t Scoped.t -> term Scoped.t -> (term * rhs * E.t * subst) Iter.t
retrieve ~sign (idx,si) (t,st) acc
iterates on (in)equations l ?= r of givensign
and substitutionssubst
, 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