Commit 2024-11-18 05:29 6e2b040a

perf: hard-code typeclass inference in linarith (#18714) This PR modifies the linarith tactic to rely on custom copies of many lemmas, rather than the library versions of these lemmas. The difference is that the copies use high-level typeclasses (such as OrderedSemiring) rather than lower-level typeclasses (such as AddRightMono). This seems to improve linarith performance. The PR also introduces a performance test to the linarith test file, with a heartbeat limit which failed before this PR and passes (with leeway) after this PR. Zulip