module type DEP = sig end
Iterators over dependency index.
type eqs
val iter : eqs -> (Fact.Equal.t -> unit) -> Term.t -> unit
iter s f y applies f to each equality e of the
form x = a with justification rho such that x
is dependent on y.
val fold : eqs -> (Fact.Equal.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
fold s f y e accumulates, starting with e, applications
of f to each equality x = a which x dependent on y.
val for_all : eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
for_all s p y holds iff p e holds for all equalities
x = a with x dependent on y.
val exists : eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
exists s p y holds iff p e holds for all equalities
x = a with x dependent on y.
val choose : eqs -> (Fact.Equal.t -> bool) -> Term.t -> Fact.Equal.t
choose s y returns equality e of the form x = a
if x is dependent on y; otherwise, Not_found is raised.