Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr

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.
Equations
  • One or more equations did not get rendered due to their size.

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

Equations
Equations
@[export lean_grind_cutsat_assert_eq]
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_process_cutsat_eq]
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_process_cutsat_eq_lit]
Equations
  • One or more equations did not get rendered due to their size.
@[export lean_process_cutsat_diseq]
Equations
  • One or more equations did not get rendered due to their size.

Internalizes an integer 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.