def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.norm (c : EqCnstr) : EqCnstr

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.norm (c : DiseqCnstr) : DiseqCnstr

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.applyEq (a : Int) (x : Var) (c₁ : EqCnstr) (b : Int) (c₂ : DiseqCnstr) : GoalM DiseqCnstr

Given an equation c₁ containing the monomial a*x, and a disequality constraint c₂ containing the monomial b*x, eliminate x by applying substitution.

partial def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.applySubsts (c : DiseqCnstr) : GoalM DiseqCnstr

def Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.assert (c : DiseqCnstr) : GoalM Unit

def Int.Linear.Poly.pickVarToElim? (p : Poly) : Option (Int × Var)

Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.

def Int.Linear.Poly.pickVarToElim?.go (k : Int) (x : Var) (p : Poly) : Int × Var

partial def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.applySubsts (c : EqCnstr) : GoalM EqCnstr

@[export lean_grind_cutsat_assert_eq]

def Lean.Meta.Grind.Arith.Cutsat.EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit

@[export lean_process_cutsat_eq]

def Lean.Meta.Grind.Arith.Cutsat.processNewEqImpl (a b : Expr) : GoalM Unit

@[export lean_process_cutsat_diseq]

def Lean.Meta.Grind.Arith.Cutsat.processNewDiseqImpl (a b : Expr) : GoalM Unit

instance Lean.Meta.Grind.Arith.Cutsat.instBEqSupportedTermKind : BEq Lean.Meta.Grind.Arith.Cutsat.SupportedTermKind✝

def Lean.Meta.Grind.Arith.Cutsat.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit

Internalizes an integer (and Nat) expression. Here are the different cases that are handled.

• a + b when parent? is not +, ≤, or ∣
• k * a when k is a numeral and parent? is not +, *, ≤, ∣
• numerals when parent? is not +, *, ≤, ∣. Recall that we must internalize numerals to make sure we can propagate equalities back to the congruence closure module. Example: we have f 5, f x, x - y = 3, y = 2.