module View: sig .. end
val get_eqn : Literals.t ->
Libzipperposition.Position.t -> (Literals.term * Literals.term * bool) option
get the term l at given position in clause, and r such that l ?= r
is the Literal.t at the given position.
Raises Invalid_argument if the position is not valid in the
val get_arith : Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t option
The following functions will raise Invalid_argument if the
position is not valid or if the literal isn't what's asked for
val get_eqn_exn : Literals.t ->
Libzipperposition.Position.t -> Literals.term * Literals.term * bool
val get_arith_exn : Literals.t -> Libzipperposition.Position.t -> ArithLit.Focus.t