Skip to content

[Merged by Bors] - chore(Condensed): shorten some names#17075

Closed
dagurtomas wants to merge 5 commits intomasterfrom
dagur/LocallyConstantGolf
Closed

[Merged by Bors] - chore(Condensed): shorten some names#17075
dagurtomas wants to merge 5 commits intomasterfrom
dagur/LocallyConstantGolf

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Sep 24, 2024 •
edited
Loading

As discussed on #15321

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 24, 2024 •
edited
Loading

PR summary c3dcd12e1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ functorIso
+ functorToPresheavesIso
- functorIsoTopCatToSheafCompHausLike
- functorToPresheavesIsoTopCatToSheafCompHausLike

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

This was referenced Sep 24, 2024
Closed
Closed
Closed
@dagurtomas dagurtomas added easy < 20s of review time. See the lifecycle page for guidelines. t-category-theory Category theory t-condensed Condensed mathematics labels Sep 24, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 25, 2024
@dagurtomas dagurtomas removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Sep 25, 2024
joelriou
joelriou reviewed Sep 25, 2024
View reviewed changes
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Sep 25, 2024

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 25, 2024

✌️ dagurtomas can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Sep 25, 2024
dagurtomas
dagurtomas commented Sep 25, 2024
View reviewed changes
dagurtomas
dagurtomas commented Sep 25, 2024
View reviewed changes
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Sep 25, 2024

Thanks!

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Sep 25, 2024
@dagurtomas
chore(Condensed): shorten some names (#17075)
65888ad
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 25, 2024

Build failed:

@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Sep 25, 2024

Sorry, I messed up merging master... I opened #17140 instead because I'm bad at git. Could I have a d+/merge on that instead?

@dagurtomas dagurtomas closed this Sep 25, 2024
@eric-wieser eric-wieser reopened this Sep 25, 2024
@eric-wieser eric-wieser force-pushed the dagur/LocallyConstantGolf branch from bd145a0 to 1250f17 Compare September 25, 2024 22:09
@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Sep 25, 2024

Let's try again

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Sep 25, 2024
@dagurtomas @eric-wieser
chore(Condensed): shorten some names (#17075)
34e653f 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Condensed): shorten some names [Merged by Bors] - chore(Condensed): shorten some names Sep 25, 2024
@mathlib-bors mathlib-bors bot closed this Sep 25, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/LocallyConstantGolf branch September 25, 2024 22:38
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Sep 26, 2024

No deprecations?

@dagurtomas
Copy link
Copy Markdown
Contributor Author

dagurtomas commented Sep 26, 2024

This is code that was initially added only a few days ago so I think it's fine not to add deprecations

fbarroero pushed a commit that referenced this pull request Oct 2, 2024
@dagurtomas @eric-wieser @fbarroero
chore(Condensed): shorten some names (#17075)
ea4435f 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). easy < 20s of review time. See the lifecycle page for guidelines. t-category-theory Category theory t-condensed Condensed mathematics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@dagurtomas @joelriou @Ruben-VandeVelde @eric-wieser @leanprover-community-bot-assistant