[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17917
[Merged by Bors] - chore: remove CoeFun instances where FunLike is available#17917Vierkantor wants to merge 1 commit intomasterfrom
CoeFun instances where FunLike is available#17917Conversation
CoeFun instances where FunLike is available
|
!bench |
PR summary 966a66bda2Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
|
Here are the benchmark results for commit 469ff48. Benchmark Metric Change
===================================================================
- ~Mathlib.Analysis.InnerProductSpace.Adjoint instructions 8.5% |
|
Nearly there! |
469ff48 to
b0a7bee
Compare
|
!bench |
|
Here are the benchmark results for commit b0a7bee. |
|
bors d+ |
|
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
|
This PR/issue depends on: |
b0a7bee to
966a66b
Compare
|
!bench |
|
Just to make sure the situation didn't change. |
|
Here are the benchmark results for commit 966a66b.Found no runs to compare against. |
|
Don't see any important changes compared to the most recent run #17656: http://speed.lean-fro.org/mathlib4/compare/20e5d4c7-6d0e-4646-b2cd-0ac15f5b729b/to/e7b27246-a3e6-496a-b552-ff4b45c7236e?hash2=1404d2bd157a39d32b67ba6655cccb6c4d50e799 So: bors merge |
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This contains everything except the interval [1/4, 3/8] of the changes, and doesn't affect the benchmark.
|
Pull request successfully merged into master. Build succeeded: |
CoeFun instances where FunLike is availableCoeFun instances where FunLike is available
During the port we found that
FunLikeis robust enough not to need an extraCoeFunshortcut. Let's see if that rule can be consistently applied to the whole of the library.There is still duplication between
FunLikeandCoeFunforGrp,Mon,CommGrpandCommMon, which will need a more thorough fix. See also #17866.This contains everything except the interval [1/4, 3/8] of the changes, and doesn't affect the benchmark.