Commit 2023-11-18 22:29 5d29e6c3

View on Github →

refactor: fold isStrictIntComparison into mkNonstrictIntProof in Linarith.Preprocessing (#8488) Implements the refactor proposed in https://github.com/leanprover-community/mathlib4/pull/8310#issuecomment-1817330246.

Estimated changes