-
Notifications
You must be signed in to change notification settings - Fork 330
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: Rename Embedding
to IsEmbedding
#18133
Conversation
PR summary 92a89f313fImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
6d3503f
to
c904a25
Compare
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards 1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Embedding` is) 2. namespacing it inside `Topology`
0487dee
to
50101ed
Compare
bors d+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards 1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Embedding` is) 2. namespacing it inside `Topology`
Build failed (retrying...): |
`Function.Embedding` is a type while `Embedding` is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towards 1. renaming `Embedding` to `IsEmbedding` and similarly for neighboring declarations (which `Embedding` is) 2. namespacing it inside `Topology`
Pull request successfully merged into master. Build succeeded: |
Embedding
to IsEmbedding
Embedding
to IsEmbedding
Function.Embedding
is a type whileEmbedding
is a proposition, and there are many other kinds of embeddings than topological embeddings. Hence this PR is a step towardsEmbedding
toIsEmbedding
and similarly for neighboring declarationsTopology