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

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

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

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

def Int.Linear.Poly.isNegEq (p₁ p₂ : Poly) : Bool

def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.erase (c : LeCnstr) : GoalM Unit

@[export lean_grind_cutsat_assert_le]

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

def Lean.Meta.Grind.Arith.Cutsat.propagateIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit

Given an expression e that is in True (or False equivalence class), if e is an integer inequality, asserts it to the cutsat state.

def Lean.Meta.Grind.Arith.Cutsat.propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit

def Lean.Meta.Grind.Arith.Cutsat.propagateIfSupportedLe (e : Expr) (eqTrue : Bool) : GoalM Unit