Skip to content

feat: add min and max list operations #11060

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.

Sign up for GitHub

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

Jump to bottom
Merged
TwoFX merged 6 commits into from
Nov 10, 2025
Merged

feat: add min and max list operations #11060

TwoFX merged 6 commits into from
Nov 10, 2025

Conversation

@ecyrbe
Copy link
Contributor

@ecyrbe ecyrbe commented Nov 2, 2025

This PR add list min and max operations to complement min? and max? ones in the same vain as head? and head.

It was dicussed here in zulip

it also add small unit tests for min , max, min? and max?

@ecyrbe ecyrbe requested review from digama0 and kim-em as code owners November 2, 2025 10:58
@TwoFX TwoFX added the changelog-library Library label Nov 2, 2025
Rob23oba
Rob23oba suggested changes Nov 2, 2025
View reviewed changes
Copy link
Contributor

@Rob23oba Rob23oba left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some small changes regarding style and naming convention.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 2, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 2, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-02 11:52:19)
  • ✅ Mathlib branch lean-pr-testing-11060 has successfully built against this PR. (2025-11-03 13:01:15) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 2, 2025

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-02 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-02 11:52:21)

@ecyrbe
Copy link
Contributor Author

ecyrbe commented Nov 2, 2025

@Rob23oba thanks for the review

kim-em
kim-em reviewed Nov 3, 2025
View reviewed changes
kim-em
kim-em reviewed Nov 3, 2025
View reviewed changes
kim-em
kim-em reviewed Nov 3, 2025
View reviewed changes
@ecyrbe
Copy link
Contributor Author

ecyrbe commented Nov 3, 2025

@kim-em added all @TwoFX lemmas from the zullip conversation and cleaned lemmas and tests as suggested.

linesthatinterlace
linesthatinterlace reviewed Nov 3, 2025
View reviewed changes
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Nov 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11060
00dad01
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 3, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11060
5d2e5e0
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Nov 3, 2025
TwoFX
TwoFX approved these changes Nov 10, 2025
View reviewed changes
Copy link
Member

@TwoFX TwoFX left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@TwoFX TwoFX added this pull request to the merge queue Nov 10, 2025
Merged via the queue into leanprover:master with commit 6008c0d Nov 10, 2025
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@TwoFX TwoFX TwoFX approved these changes

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

+2 more reviewers

@linesthatinterlace linesthatinterlace linesthatinterlace left review comments

@Rob23oba Rob23oba Rob23oba requested changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@ecyrbe @leanprover-community-bot @leanprover-bot @kim-em @TwoFX @linesthatinterlace @Rob23oba