[Merged by Bors] - perf (Data.Rat): reduce algebra instances for Rat#6282
[Merged by Bors] - perf (Data.Rat): reduce algebra instances for Rat#6282mattrobball wants to merge 3 commits intomasterfrom
Conversation
|
!bench |
|
Here are the benchmark results for commit 7a00598. Benchmark Metric Change
==================================================================
+ ~Mathlib.Data.Rat.Basic instructions -15.3%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers instructions -7.3% |
|
Currently there are commented-out sanity test My suggestion: the reviewer should pull a copy, un-comment, and check the two files compile. Then if they are happy, tell me to delete them. Very much open to other suggestions. |
|
Removing those comments seems fine to me. I think in the long run we should have a linter to catch diamonds here. |
|
bors d+ |
|
✌️ mattrobball can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
This removes the `with` pattern from the `Field` and `CommSemiGroupWithZero` instances on `Rat`. The resulting term decreases in size by an order of magnitude (at least). Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
This removes the `with` pattern from the `Field` and `CommSemiGroupWithZero` instances on `Rat`. The resulting term decreases in size by an order of magnitude (at least). Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
This removes the `with` pattern from the `Field` and `CommSemiGroupWithZero` instances on `Rat`. The resulting term decreases in size by an order of magnitude (at least). Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
This removes the `with` pattern from the `Field` and `CommSemiGroupWithZero` instances on `Rat`. The resulting term decreases in size by an order of magnitude (at least). Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
This removes the
withpattern from theFieldandCommSemiGroupWithZeroinstances onRat.The resulting term decreases in size by an order of magnitude (at least).