[Merged by Bors] - chore(Order/BooleanAlgebra): golf entire diff_insert_of_notMem, insert_diff_of_mem, insert_diff_of_notMem and subset_insert_iff using grind#28628
Conversation
euprunin
commented
Aug 19, 2025
PR summary 59c724d051Import 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
|
|
Can you say something about the performance of this change - and bundle with other Order PR, please? Thanks! |
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind`
80aa599 to
fdc159a
Compare
|
!bench |
|
Here are the benchmark results for commit fdc159a. |
2 files, Instructions -2.0⬝10⁹
|
|
@grunweg Thanks for reviewing! Based on the !bench results this change seems to be performance neutral. |
grunweg
left a comment
There was a problem hiding this comment.
Thanks!
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
|
Thanks! |
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` (#28628)
|
Build failed (retrying...): |
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` (#28628)
|
Pull request successfully merged into master. Build succeeded: |
diff_insert_of_notMem, insert_diff_of_mem, insert_diff_of_notMem and subset_insert_iff using grinddiff_insert_of_notMem, insert_diff_of_mem, insert_diff_of_notMem and subset_insert_iff using grind
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` (leanprover-community#28628)
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` (leanprover-community#28628)
…sert_diff_of_mem`, `insert_diff_of_notMem` and `subset_insert_iff` using `grind` (leanprover-community#28628)