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] - style: use cases x with | ...
instead of cases x; case => ...
#9321
Conversation
!bench |
Here are the benchmark results for commit 2581c17. |
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alexjbest. |
Btw, to what extent was this automatically generated? |
Not at all, although I did think about ways this kind of thing might be automated in the future. |
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.
Thanks 🎉
bors merge
) This converts usages of the pattern ```lean cases h case inl h' => ... case inr h' => ... ``` which derive from mathported code, to the "structured `cases`" syntax: ```lean cases h with | inl h' => ... | inr h' => ... ``` The case where the subgoals are handled with `·` instead of `case` is more contentious (and much more numerous) so I left those alone. This pattern also appears with `cases'`, `induction`, `induction'`, and `rcases`. Furthermore, there is a similar transformation for `by_cases`: ```lean by_cases h : cond case pos => ... case neg => ... ``` is replaced by: ```lean if h : cond then ... else ... ``` Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Pull request successfully merged into master. Build succeeded: |
cases x with | ...
instead of cases x; case => ...
cases x with | ...
instead of cases x; case => ...
This converts usages of the pattern
which derive from mathported code, to the "structured
cases
" syntax:cases h with | inl h' => ... | inr h' => ...
The case where the subgoals are handled with
·
instead ofcase
is more contentious (and much more numerous) so I left those alone. This pattern also appears withcases'
,induction
,induction'
, andrcases
. Furthermore, there is a similar transformation forby_cases
:is replaced by: