-
Notifications
You must be signed in to change notification settings - Fork 297
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] - doc(field_theory/splitting_field): update code example to reflect changes to diamond issues #15620
Conversation
…nges to diamond issues
c21a37f
to
243c99c
Compare
Let me see if I can't just fix this before we update the docs to say it can't be fixed... |
I wouldn't say the docs says "this can't be fixed", they just more clearly say "this is broken" and remove the now-invalid excuse! |
@Vierkantor could you please take another look? You've been working on the |
Alright, let's merge this for now because the diamond is rather evil... bors r+ |
…nges to diamond issues (#15620) We now have infrastructure in place to avoid diamonds in nat/int/rat algebras, so we can't appeal to a lack of it when explaining diamond issues.
Pull request successfully merged into master. Build succeeded: |
…nges to diamond issues (leanprover-community#15620) We now have infrastructure in place to avoid diamonds in nat/int/rat algebras, so we can't appeal to a lack of it when explaining diamond issues.
…nges to diamond issues (#15620) We now have infrastructure in place to avoid diamonds in nat/int/rat algebras, so we can't appeal to a lack of it when explaining diamond issues.
…nges to diamond issues (#15620) We now have infrastructure in place to avoid diamonds in nat/int/rat algebras, so we can't appeal to a lack of it when explaining diamond issues.
We now have infrastructure in place to avoid diamonds in nat/int/rat algebras, so we can't appeal to a lack of it when explaining diamond issues.