Skip to content

feat: improve Ord proof api #8378

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
merged 5 commits into from
May 23, 2025
Merged

feat: improve Ord proof api #8378

merged 5 commits into from
May 23, 2025

Conversation

Rob23oba
Copy link
Contributor

This PR improves and extends the api around Ord and Ordering. These changes are split off from #8210.

@Rob23oba Rob23oba requested review from TwoFX and kim-em as code owners May 16, 2025 09:29
@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels May 16, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 16, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 528fe0b0ed673accd37d986d80a7c49f876a3087 --onto 6ca31baa55e4b29c9667085736863f9ca840b16c. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-16 09:57:15)
  • ✅ Mathlib branch lean-pr-testing-8378 has successfully built against this PR. (2025-05-21 11:16:07) View Log

datokrat
datokrat reviewed May 21, 2025
View reviewed changes
datokrat
datokrat approved these changes May 21, 2025
View reviewed changes
Copy link
Contributor

@datokrat datokrat left a comment

Choose a reason for hiding this comment

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

Looks very nice to me, thanks!

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8378
25f982d
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8378
e9e6d5c
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 21, 2025
@datokrat datokrat added this pull request to the merge queue May 23, 2025
Merged via the queue into leanprover:master with commit 65a5d0c May 23, 2025
19 checks passed
@Rob23oba Rob23oba deleted the improve-ord-api branch May 23, 2025 14:36
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@datokrat datokrat datokrat approved these changes

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

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

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.
3 participants
@Rob23oba @leanprover-community-bot @datokrat