Skip to content

[Merged by Bors] - chore(Combinatorics/SimpleGraph): remove sndOfNotNil#16352

Closed
pimotte wants to merge 1 commit intomasterfrom
PO_fix_sndOfNotNil
Closed

[Merged by Bors] - chore(Combinatorics/SimpleGraph): remove sndOfNotNil#16352
pimotte wants to merge 1 commit intomasterfrom
PO_fix_sndOfNotNil

Conversation

@pimotte
Copy link
Copy Markdown
Collaborator

@pimotte pimotte commented Aug 31, 2024 •
edited by YaelDillies
Loading

Readd the refactorings to sndOfNotNil and tail

The changes in 17b10a9 were accidentally reverted in 5025874
This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in Hamiltonian.lean which I fixed.

Open in Gitpod

I conferred with @semorrison and they mentioned that it looked like an accident with the adaptation branch in #15513
Original PR: #15237

@pimotte pimotte added the t-combinatorics Combinatorics label Aug 31, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 31, 2024

PR summary 554ca183dd

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ adj_getVert_one
+ drop
+ getVert_cons
+ getVert_cons_one
+ getVert_cons_succ
+ getVert_copy
+ not_nil_iff_lt_length
+ support_tail_of_not_nil
+ tail_cons_eq
+ tail_cons_nil
- adj_sndOfNotNil
- cons_getVert
- cons_getVert_succ
- cons_sndOfNotNil
- getVert_one
- sndOfNotNil
- tail_support_eq_support_tail

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.

@Command-Master
Copy link
Copy Markdown
Collaborator

Command-Master commented Sep 1, 2024 •
edited
Loading

I just noticed this, it conflicts with #16382. I think this should be merged and I'll edit my PR to keep whatever's relevant

@Command-Master Command-Master mentioned this pull request Sep 1, 2024
Closed
2 tasks
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Sep 1, 2024

Thank you for the persistence!

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Sep 1, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Sep 1, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented Sep 4, 2024

Thanks! 🎉
bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 4, 2024
mathlib-bors bot pushed a commit that referenced this pull request Sep 4, 2024
@pimotte
chore(Combinatorics/SimpleGraph): remove sndOfNotNil (#16352)
2675050 
Readd the refactorings to sndOfNotNil and tail

The changes in 17b10a9 were accidentally reverted in 5025874
This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in `Hamiltonian.lean` which I fixed.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 4, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Combinatorics/SimpleGraph): remove sndOfNotNil [Merged by Bors] - chore(Combinatorics/SimpleGraph): remove sndOfNotNil Sep 4, 2024
@mathlib-bors mathlib-bors bot closed this Sep 4, 2024
@mathlib-bors mathlib-bors bot deleted the PO_fix_sndOfNotNil branch September 4, 2024 02:18
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@pimotte @bjoernkjoshanssen
chore(Combinatorics/SimpleGraph): remove sndOfNotNil (#16352)
20bbdf0 
Readd the refactorings to sndOfNotNil and tail

The changes in 17b10a9 were accidentally reverted in 5025874
This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in `Hamiltonian.lean` which I fixed.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@pimotte @bjoernkjoshanssen
chore(Combinatorics/SimpleGraph): remove sndOfNotNil (#16352)
f85597c 
Readd the refactorings to sndOfNotNil and tail

The changes in 17b10a9 were accidentally reverted in 5025874
This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in `Hamiltonian.lean` which I fixed.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@pimotte @bjoernkjoshanssen
chore(Combinatorics/SimpleGraph): remove sndOfNotNil (#16352)
2a6e63d 
Readd the refactorings to sndOfNotNil and tail

The changes in 17b10a9 were accidentally reverted in 5025874
This PR reintroduces the changes. The patch applied cleanly, except for some small conflict in `Hamiltonian.lean` which I fixed.
@SnirBroshi SnirBroshi mentioned this pull request Nov 23, 2025
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@pimotte @Command-Master @YaelDillies @urkud