-
Notifications
You must be signed in to change notification settings - Fork 259
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] - chore(Topology/Homeomorph): rename type variables #7587
Conversation
I don't quite understand the build errors and have asked on Zulip. Help welcome! |
Found a fix, I think. |
1fe657b
to
8ccee1f
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!
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!
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.
Oh I saw the problems found by @eric-wieser in the other PR, so I took a closer look. Fortunately, there aren't much that could go wrong in this file ...
Thank you for the fast review. I have addressed all comments (and also renamed an equivalence |
I'm puzzled by the build failures; I don't know enough to fix them. Help appreciated. |
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
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 🎉
bors merge
X, Y, Z are standard mathematical names for topological spaces. As [discussed](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention.3A.20topological.20spaces/near/395769893) on zulip, let us rename them. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Canceled. |
@jcommelin I've merged master (to adapt the changes in #7595 as well). Can you approve again, please? |
Thanks 🎉 bors merge |
X, Y, Z are standard mathematical names for topological spaces. As [discussed](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Naming.20convention.3A.20topological.20spaces/near/395769893) on zulip, let us rename them. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
X, Y, Z are standard mathematical names for topological spaces.
As discussed on zulip, let us rename them.