def Lean.Meta.Grind.Arith.Cutsat.LeCnstr.norm (c : LeCnstr) : 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.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.

Equations

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

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

Equations

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

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

Equations

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