Module Literal.View

module View: sig .. end

val as_eqn : Literal.t -> (Literal.term * Literal.term * bool) option

val get_eqn : Literal.t ->
       Libzipperposition.Position.t -> (Literal.term * Literal.term * bool) option

View of a Prop or Equation literal, oriented by the position. If the position selects its left term, return l, r, otherwise r, l. for propositions it will always be p, true.
Raises Invalid_argument if the position doesn't match the literal.
Returns None for other literals

val get_arith : Literal.t -> ArithLit.t option

Extract an arithmetic literal

val focus_arith : Literal.t -> Libzipperposition.Position.t -> ArithLit.Focus.t option

Focus on a specific term in an arithmetic literal. The focused term is removed from its monome, and its coefficient is returned.

val unfocus_arith : ArithLit.Focus.t -> Literal.t