[Merged by Bors] - chore: use the positivity [h, h'] syntax when useful#30654
[Merged by Bors] - chore: use the positivity [h, h'] syntax when useful#30654grunweg wants to merge 1 commit intoleanprover-community:masterfrom
positivity [h, h'] syntax when useful#30654Conversation
PR summary 94c059e90aImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 No changes to technical debt.You can run this locally as
|
|
!bench |
|
Here are the benchmark results for commit 562c75f. |
|
|
Yes, please! And thank you! Can you please add a short blurb in the PR description saying how you found these occurrences? Was it just bors d+ |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Yes, I grepped (added that to the PR description) --- and just realised why I only found so few hits. Thanks for the inspiration, follow-up incoming :-) |
|
bors merge |
Since #30388, `have := foo; positivity` can be shortened to `positivity [foo]`. Make use of that when sensible. I searched for all occurrences of `have :.*\n\s*positi` (using VS Code, i.e. using `rg` internally) and inspected them manually. In a few cases, keeping the `have` separate seemed more readable to me.
|
Update: searching for |
|
Filed the follow-up as #30656. |
|
Pull request successfully merged into master. Build succeeded: |
positivity [h, h'] syntax when usefulpositivity [h, h'] syntax when useful
Continuation of #30654.
…mmunity#30654) Since leanprover-community#30388, `have := foo; positivity` can be shortened to `positivity [foo]`. Make use of that when sensible. I searched for all occurrences of `have :.*\n\s*positi` (using VS Code, i.e. using `rg` internally) and inspected them manually. In a few cases, keeping the `have` separate seemed more readable to me.
…mmunity#30654) Since leanprover-community#30388, `have := foo; positivity` can be shortened to `positivity [foo]`. Make use of that when sensible. I searched for all occurrences of `have :.*\n\s*positi` (using VS Code, i.e. using `rg` internally) and inspected them manually. In a few cases, keeping the `have` separate seemed more readable to me.
Since #30388,
have := foo; positivitycan be shortened topositivity [foo].Make use of that when sensible.
I searched for all occurrences of
have :.*\n\s*positi(using VS Code, i.e. usingrginternally) and inspected them manually. In a few cases, keeping thehaveseparate seemed more readable to me.