-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor: drop some *HomClass
es
#10544
Conversation
Drop classes that mix `OrderHomClass` with algebraic hom classes.
@[to_additive (attr := coe) | ||
"Turn an element of a type `F` satisfying `OrderAddMonoidHomClass F α β` into an actual | ||
`OrderAddMonoidHom`. This is declared as the default coercion from `F` to `α →+o β`."] | ||
def OrderMonoidHomClass.toOrderMonoidHom [OrderMonoidHomClass F α β] (f : F) : α →*o β := | ||
{ (f : α →* β) with monotone' := monotone f } | ||
def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a bit weird to put this in the OrderMonoidHomClass
namespace given that such a class doesn't exist anymore, but I don't have a better suggestion.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
How about
def OrderMonoidHomClass.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : | |
def FunLike.toOrderMonoidHom [OrderHomClass F α β] [MonoidHomClass F α β] (f : F) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Let me do it for all bundled homs at once.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Very nice!
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |
*HomClass
es*HomClass
es
Drop classes that mix
OrderHomClass
with algebraic hom classes.