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

Equations

• c.norm = if c.p.isSorted = true then c else { p := c.p.norm, h := Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.norm c }

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

Equations

• c.norm = if c.p.isSorted = true then c else { p := c.p.norm, h := Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.norm c }

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.

Equations

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

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

Equations

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

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.

Equations

• (Int.Linear.Poly.num k).pickVarToElim? = none
• (Int.Linear.Poly.add k' x' p_2).pickVarToElim? = some (Int.Linear.Poly.pickVarToElim?.go k' x' p_2)

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

Equations

• One or more equations did not get rendered due to their size.
• Int.Linear.Poly.pickVarToElim?.go k x (Int.Linear.Poly.num k_1) = if (k == 1 || k == -1) = true then (k, x) else (k, x)

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

Equations

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

@[export lean_process_cutsat_eq]

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

Equations

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

@[export lean_process_cutsat_diseq]

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

Equations

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

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.instBEqSupportedTermKind = { beq := Lean.Meta.Grind.Arith.Cutsat.beqSupportedTermKind✝ }

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.

Equations

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