type t = | Left of op * Z.t Monome.Focus.t * Z.t Monome.t| Right of op * Z.t Monome.t * Z.t Monome.Focus.t| Div of Z.t Monome.Focus.t dividesfocus on a term in one of the two monomes
val mk_div : ?sign:bool -> Z.t -> power:int -> Z.t Monome.Focus.t -> tval get : lit -> Position.t -> t optionval get_exn : lit -> Position.t -> tInvalid_argument if the position doesn't fit
Attempt to focus on the given atomic term, if it occurs directly under the arith literal
replace a m replaces mf.coeff × mf.term with m where mf is the focused monome in a, and return the resulting literal
val focused_monome : t -> Z.t Monome.Focus.tThe focused monome
Unsafe version of opposite_monome.
Invalid_argument if the literal is a Div
val is_max : ord:Ordering.t -> t -> boolIs the focused term maximal in the literal?
val is_strictly_max : ord:Ordering.t -> t -> boolIs the focused term maximal in the literal, ie is it greater than all the other terms?
val map_lit :
f_m:(Z.t Monome.t -> Z.t Monome.t) ->
f_mf:(Z.t Monome.Focus.t -> Z.t Monome.Focus.t) ->
t ->
tApply a function to the monomes and focused monomes
Multiply the two literals by some constant so that their focused literals have the same coefficient
For a "divides" literal, bring it to the given power.
Invalid_argument if the current power is strictly greater than the argument (cannot scale down), or if the literal is not a Div
val apply_subst : Subst.Renaming.t -> Subst.t -> t Scoped.t -> tApply a substitution
val unify :
?subst:Unif_subst.t ->
t Scoped.t ->
t Scoped.t ->
(t * t * Unif_subst.t) Iter.tUnify the two focused terms, and possibly other terms of their respective focused monomes; yield the new literals accounting for the unification along with the unifier
val fold_terms : ?pos:Position.t -> lit -> (t * Position.t) Iter.tFold on focused terms in the literal, one by one, with the position of the focused term
val pp : t CCFormat.printerval to_string : t -> string