[Merged by Bors] - chore: further backports for leanprover/lean4#6397#20098
[Merged by Bors] - chore: further backports for leanprover/lean4#6397#20098
Conversation
PR summary 2b7a00e3bfImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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
|
|
|
||
| theorem countP_of (x : α) : countP p (of x) = if p x = true then 1 else 0 := by | ||
| simp [countP, List.countP, List.countP.go] | ||
| change List.countP p [x] = _ |
There was a problem hiding this comment.
Should we have a simp(?) lemma that brings the LHS in this form?
There was a problem hiding this comment.
No, I don't think we should, unless someone actually adds the explicit conversion from FreeMonoid to List. As is, it is defeq abuse.
There was a problem hiding this comment.
There was a problem hiding this comment.
Aah, thanks for that pointer to zulip.
In that case, I suggest we also leave a comment at the top of the file with the same comments as (or a pointer to) that zulip thread.
| theorem count_of [DecidableEq α] (x y : α) : count x (of y) = (Pi.single x 1 : α → ℕ) y := by | ||
| simp [Pi.single, Function.update, count, countP, List.countP, List.countP.go, | ||
| Bool.beq_eq_decide_eq] | ||
| change List.count x [y] = _ |
There was a problem hiding this comment.
That lemma would then also apply here, I suppose.
|
bors d+ |
|
✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Build failed (retrying...): |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Build failed (retrying...): |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Build failed: |
|
bors merge |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Build failed (retrying...): |
Co-authored-by: Johan Commelin <johan@commelin.net>
|
Pull request successfully merged into master. Build succeeded: |
No description provided.