[Merged by Bors] - chore(Filter/Prod): drop Filter.prod, use SProd instead#18315
[Merged by Bors] - chore(Filter/Prod): drop Filter.prod, use SProd instead#18315
Filter.prod, use SProd instead#18315Conversation
PR summary 7592d0f53eImport 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 Decrease in tech debt: (relative, absolute) = (3.00, 0.00)
Current commit 7592d0f53e You can run this locally as
|
|
|
||
| /-- Product of filters. This is the filter generated by cartesian products | ||
| of elements of the component filters. -/ | ||
| protected def prod (f : Filter α) (g : Filter β) : Filter (α × β) := |
There was a problem hiding this comment.
Should I leave it as a deprecated definition?
There was a problem hiding this comment.
I would say: yes, out of principle. Dealing with deprecations is much nicer than dealing with removed definitions.
grunweg
left a comment
There was a problem hiding this comment.
Does what it says on the tin. Can you add a sentence why you're doing this?
maintainer merge
|
|
||
| /-- Product of filters. This is the filter generated by cartesian products | ||
| of elements of the component filters. -/ | ||
| protected def prod (f : Filter α) (g : Filter β) : Filter (α × β) := |
There was a problem hiding this comment.
I would say: yes, out of principle. Dealing with deprecations is much nicer than dealing with removed definitions.
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
bors d+ |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
As this PR is labelled bors merge |
This way we can't accidentally use the underlying `Filter.prod` instead of the normal form.
|
Pull request successfully merged into master. Build succeeded: |
Filter.prod, use SProd insteadFilter.prod, use SProd instead
This way we can't accidentally use the underlying
Filter.prodinstead of the normal form.