Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - chore(data/*): Removing unnecessary simp lemmas #17062

Closed
wants to merge 6 commits into from
Closed

[Merged by Bors] - chore(data/*): Removing unnecessary simp lemmas #17062

wants to merge 6 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Oct 19, 2022 •
edited by alreadydone
Loading

Open in Gitpod

@BoltonBailey BoltonBailey added the WIP Work in progress label Oct 19, 2022
BoltonBailey and others added 3 commits October 19, 2022 17:58
@BoltonBailey @eric-wieser
Update scripts/simp_golfing.py
74e5d1c 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@BoltonBailey @eric-wieser
Update scripts/simp_golfing.py
c84a309 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@BoltonBailey
Update typevec.lean
8f0b8c2
alreadydone
alreadydone reviewed Oct 19, 2022
View reviewed changes
src/data/pequiv.lean Outdated Show resolved Hide resolved
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Oct 20, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 1, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@semorrison
Copy link
Collaborator

@BoltonBailey, do you want to mark this as ready for review? The incoming tide of mathlib4 porting is about to wash over these files. :-)

@BoltonBailey
Copy link
Collaborator Author

@BoltonBailey, do you want to mark this as ready for review? The incoming tide of mathlib4 porting is about to wash over these files. :-)

Yeah I was holding off because the python file wasn't well-written enough but that should really probably be a separate PR anyway. I'll remove the script and mark ready-for-review.

@BoltonBailey BoltonBailey added awaiting-CI The author would like to see what CI has to say before doing more work. and removed WIP Work in progress labels Nov 18, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Nov 18, 2022
@BoltonBailey BoltonBailey added the awaiting-review The author would like community review of the PR label Nov 18, 2022
@BoltonBailey
Copy link
Collaborator Author

@semorrison Also, ultimately these changes are not very important, so I would certainly rather this PR be closed without merging than have it step on the toes of the porting in any way.

@alreadydone
Copy link
Collaborator

maintainer merge

@github-actions
Copy link

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

@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Nov 19, 2022
bors bot pushed a commit that referenced this pull request Nov 19, 2022
@BoltonBailey
chore(data/*): Removing unnecessary simp lemmas (#17062)
bcb06bc 
This PR adds a script that looks for and removes unnecessary lemmas in simp calls.

- [x] depends on: #17078
@bors
Copy link

bors bot commented Nov 19, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Nov 19, 2022
@BoltonBailey
chore(data/*): Removing unnecessary simp lemmas (#17062)
4fcbc82 
This PR adds a script that looks for and removes unnecessary lemmas in simp calls.

- [x] depends on: #17078
@bors
Copy link

bors bot commented Nov 19, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title chore(data/*): Removing unnecessary simp lemmas [Merged by Bors] - chore(data/*): Removing unnecessary simp lemmas Nov 19, 2022
@bors bors bot closed this Nov 19, 2022
@bors bors bot deleted the BoltonBailey/simp_rw-linting branch November 19, 2022 14:35
@BoltonBailey BoltonBailey mentioned this pull request Aug 24, 2023
Closed
@BoltonBailey BoltonBailey mentioned this pull request Dec 15, 2023
Closed
1 task
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@alreadydone alreadydone alreadydone left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@BoltonBailey @mathlib-dependent-issues-bot @semorrison @alreadydone @eric-wieser