def Lean.Meta.Grind.Arith.Cutsat.mkLeCnstr (p : Poly) (h : LeCnstrProof) : GoalM LeCnstr

Equations

• Lean.Meta.Grind.Arith.Cutsat.mkLeCnstr p h = do let __do_lift ← Lean.Meta.Grind.Arith.Cutsat.mkCnstrId pure { p := p, h := h, id := __do_lift }

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

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

Equations

• (Int.Linear.Poly.num k₁).isNegEq (Int.Linear.Poly.num k₂) = (k₁ == -k₂)
• (Int.Linear.Poly.add a₁ x p₁_2).isNegEq (Int.Linear.Poly.add a₂ y p₂_2) = (a₁ == -a₂ && x == y && p₁_2.isNegEq p₂_2)
• p₁.isNegEq p₂ = false

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Grind.Arith.Cutsat.propagateIfIntLe (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.

Equations

• One or more equations did not get rendered due to their size.