Module Solution.SET.Dep


module 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.
Parameters:
? : eqs
? : Fact.Equal.t -> unit
? : Term.t
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.
Parameters:
? : eqs
? : Fact.Equal.t -> 'a -> 'a
? : Term.t
? : 'a
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.
Parameters:
? : eqs
? : Fact.Equal.t -> bool
? : Term.t
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.
Parameters:
? : eqs
? : Fact.Equal.t -> bool
? : Term.t
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.
Parameters:
? : eqs
? : Fact.Equal.t -> bool
? : Term.t