Skip to content

Remove two unnecessary rws#10338

Closed
darabos wants to merge 2 commits intoleanprover-community:masterfrom
darabos:darabos-unnecessary
Closed

Remove two unnecessary rws#10338
darabos wants to merge 2 commits intoleanprover-community:masterfrom
darabos:darabos-unnecessary

Conversation

@darabos
Copy link
Copy Markdown
Contributor

@darabos darabos commented Feb 7, 2024

Removes two unnecessary rw applications.

Sorry about the possibly pointless PR. I was working on something else and hit these. I think with some more effort I could find and remove all the unnecessary rw rules in Mathlib. Would that be useful? Or is it better to keep these?

Thanks!

Open in Gitpod

@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Feb 9, 2024

Hi, thanks for the pull request! Unfortunately due to technical limitations we can't review pull requests from a fork: could you please push directly to a new branch of the leanprover-community/mathlib4 repository and reopen the PR from there? I have sent you a contributor invitation so you have push access. Feel free to assign the new PR to me, then it's on my todo list.

@Vierkantor Vierkantor added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 9, 2024
@urkud
Copy link
Copy Markdown
Member

urkud commented Feb 14, 2024

I'll try to manually hit "Approve and run" button to see what happens.

@darabos
Copy link
Copy Markdown
Contributor Author

darabos commented Feb 17, 2024

Hi, thanks for the pull request! Unfortunately due to technical limitations we can't review pull requests from a fork: could you please push directly to a new branch of the leanprover-community/mathlib4 repository and reopen the PR from there? I have sent you a contributor invitation so you have push access. Feel free to assign the new PR to me, then it's on my todo list.

Sorry, I took too long and the invitation expired. Could you please re-send it? Thank you! (I'll also fix the conflicts.)

@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 17, 2024
@Vierkantor
Copy link
Copy Markdown
Contributor

Vierkantor commented Feb 17, 2024

Invite resent!

@darabos darabos mentioned this pull request Feb 18, 2024
Closed
@darabos
Copy link
Copy Markdown
Contributor Author

darabos commented Feb 18, 2024

Invite resent!

Got it, thanks! I've reposted this from an in-repository branch as #10704. That PR has all the unnecessary rules that I found.

@darabos darabos closed this Feb 18, 2024
@darabos darabos deleted the darabos-unnecessary branch February 18, 2024 21:40
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

awaiting-author A reviewer has asked the author a question or requested changes. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@darabos @Vierkantor @urkud