Commit 2023-04-20 04:08 32cb47a7

View on Github →

fix: discard linarith wrong type equalities, style (#2611) Mostly style fixes in linarith, but also fixes #2610

Estimated changes

Modified Mathlib/Lean/Exception.lean

added def Lean.Exception.isFailedToSynthesize

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Frontend.lean

modified def Linarith.runLinarith

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

modified def Linarith.compWithZero

modified def Linarith.natToInt

modified def Linarith.nlinarithExtras

modified def Linarith.removeNegations

modified def Linarith.strengthenStrictInt

Modified Mathlib/Tactic/Linarith/Verification.lean

Modified test/linarith.lean