Skip to content

feat: SInt ranges #10633

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
datokrat merged 14 commits into from
Oct 10, 2025
Merged

feat: SInt ranges #10633

datokrat merged 14 commits into from
Oct 10, 2025

Conversation

@datokrat
Copy link
Contributor

@datokrat datokrat commented Oct 1, 2025 •
edited
Loading

This PR provides range support for the signed finite number types Int{8,16,32,64} and ISize. The proof obligations are handled by reducing all of them to proofs about an internal UpwardEnumerable instance for BitVec interpreted as signed numbers.

@datokrat datokrat added the changelog-library Library label Oct 1, 2025
@datokrat datokrat force-pushed the paul/base/ranges/sint branch from c1cb1a5 to 79f4871 Compare October 2, 2025 12:32
@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 Oct 2, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Oct 2, 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 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d88e417cda0f7afb1e15c806c6bfdbbb09ba7eef. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-02 13:20:49)
  • ✅ Mathlib branch lean-pr-testing-10633 has successfully built against this PR. (2025-10-08 22:24:00) View Log
  • ✅ Mathlib branch lean-pr-testing-10633 has successfully built against this PR. (2025-10-09 09:10:16) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Oct 2, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 24c86fc05d5abeb147be04275fe6945d39f6b8c3 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-02 13:20:51)
  • 🟡 Reference manual branch lean-pr-testing-10633 build against this PR didn't complete normally. (2025-10-08 21:31:41) View Log
  • ✅ Reference manual branch lean-pr-testing-10633 has successfully built against this PR. (2025-10-08 21:32:02) View Log
  • 🟡 Reference manual branch lean-pr-testing-10633 build against this PR didn't complete normally. (2025-10-09 08:16:37) View Log
  • ✅ Reference manual branch lean-pr-testing-10633 has successfully built against this PR. (2025-10-09 08:16:58) View Log

@datokrat datokrat force-pushed the paul/base/ranges/sint branch from 79f4871 to 54c6efe Compare October 8, 2025 20:20
@datokrat datokrat changed the base branch from paul/base/ranges/sint to master October 8, 2025 20:20
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10633
3f8973e
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#10633
095c897
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Oct 8, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#10633
43b178e
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Oct 8, 2025
@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 8, 2025
@datokrat datokrat marked this pull request as ready for review October 9, 2025 07:20
@datokrat datokrat requested a review from kim-em as a code owner October 9, 2025 07:20
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10633
f6ef1a2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Oct 9, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#10633
64f224b
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Oct 9, 2025
@leanprover-bot
Update lean-toolchain for leanprover/lean4#10633
41ce57f
@datokrat datokrat added this pull request to the merge queue Oct 10, 2025
Merged via the queue into master with commit 3931a72 Oct 10, 2025
18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX TwoFX approved these changes

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

Assignees

No one assigned

Labels

builds-manual CI has verified that the Lean Language Reference builds against this PR 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.

5 participants

@datokrat @leanprover-community-bot @leanprover-bot @TwoFX