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] - feat(algebra/pointwise): make instances global #3240
Conversation
dc12523
to
8a639a8
Compare
I'm currently simplifying I'm haven't yet done anything specifically for I think I can finish this tomorrow (depending on the number of errors left). |
16fb49e
to
4135264
Compare
Please fix merge conflicts. |
I will, but feel free to already review the current version. |
much cleanup make many variables implicit make many names shorter add some lemmas add type set_semiring as alias for set, with appropriate instance
531edc5
to
83bc3c3
Compare
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.
Thanks 🎉
Now that this compiles, I'm happy to kick it on the queue!
bors merge
add image2 and image3, the images of binary and ternary functions cleanup in algebra/pointwise make many variables implicit make many names shorter add some lemmas add more simp lemmas add type set_semiring as alias for set, with semiring instance using union as "addition"
Pull request successfully merged into master. Build succeeded: |
…3240) add image2 and image3, the images of binary and ternary functions cleanup in algebra/pointwise make many variables implicit make many names shorter add some lemmas add more simp lemmas add type set_semiring as alias for set, with semiring instance using union as "addition"
Move `set_semiring` to a new file `data.set.semiring`. Crediting Floris for #3240 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
add image2 and image3, the images of binary and ternary functions
cleanup in algebra/pointwise
make many variables implicit
make many names shorter
add some lemmas
add more simp lemmas
add type set_semiring as alias for set, with semiring instance using union as "addition"