-
Notifications
You must be signed in to change notification settings - Fork 251
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: remove stream-of-consciousness uses of have
, replace
and suffices
#10640
Conversation
This syntax remains available downstream with `import Mathlib.Tactic`, but is not available in mathlib
…eanprover-community/mathlib4 into eric-wieser/remove-tactic.Have
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have not read the diff, but I am keen in principle to get this merged.
I have reverted the two noisy tests to the previous versions, which are non-noisy but use the old-fashioned have. I think this shouldn't block this PR, since remaining issues can be discussed in #10534 while here we are just doing a cleanup of the library, which doesn't have to be complete. |
bors merge |
Pull request successfully merged into master. Build succeeded: |
have
, replace
and suffices
have
, replace
and suffices
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
…mathlib (#10534) This syntax remains available downstream with `import Mathlib.Tactic`, but is no longer available in mathlib itself. This follows on from #10640, which remove all current uses of this syntax. By removing these imports, we prevent further regressions in mathlib, and save reviewers from having to look out for this in review. In future we could delete this syntax entirely, but this would harm downstream code, especially mathport output. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
No changes to tactic file, it's just boring fixes throughout the library.
This follows on from #6964.
The fixes have been found by disabling the tactics, in #10534, but the current PR does not touch the tactic files to make it easier to review and uncontroversial.
After this PR, there are just two remaining uses of the old style
have
, intest/slim_check
, which I don't know how to convert to the new style without making them noisy (plus the other ones that will have been introduced to master in between!)