[Merged by Bors] - feat(Data.DFinsupp.Notation): add notation for DFinsupp#10962
[Merged by Bors] - feat(Data.DFinsupp.Notation): add notation for DFinsupp#10962eric-wieser wants to merge 12 commits intomasterfrom
DFinsupp#10962Conversation
This just extends the existing notation we already use for `Finsupp`
DFinsupp`DFinsupp
Co-authored-by: Timo Carlin-Burns <timorcb@gmail.com>
joneugster
left a comment
There was a problem hiding this comment.
This looks like a very clean and short PR to me.
Hopefully it should be easy for a reviewer to delegate/merge!
Only question I have is whether there is any test-case for Finsupp which ensures the notation for Finsupp takes priority over DFinsupp, and if not, then maybe one could be added.
Indeed, in the presence of both imports breaks things |
This is now fixed. |
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks, that's very nice!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
Pull request successfully merged into master. Build succeeded: |
DFinsuppDFinsupp
This just extends the existing notation we already use for
Finsupp(#6367).The two seem to coexist on the same notation without any issue.