Skip to content

feat: Fin and Char ranges #12058

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
Jan 22, 2026
Merged

feat: Fin and Char ranges #12058

TwoFX merged 6 commits into from
Jan 22, 2026

Conversation

@TwoFX
Copy link
Member

@TwoFX TwoFX commented Jan 20, 2026 •
edited
Loading

This PR implements iteration over ranges for Fin and Char.

To this end, we introduce machinery for pulling back lawfulness of UpwardEnumerable along an injective map and study the function Char.ordinal : Char -> Fin Char.numCodePoints.

@TwoFX TwoFX added the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Jan 20, 2026
@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 Jan 20, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 20, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-01-20 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. (2026-01-20 10:43:57)
  • 💥 Mathlib branch lean-pr-testing-12058 build failed against this PR. (2026-01-21 09:45:12) View Log
  • 🟡 Mathlib branch lean-pr-testing-12058 build this PR didn't complete normally. (2026-01-21 10:38:09) View Log
  • ✅ Mathlib branch lean-pr-testing-12058 has successfully built against this PR. (2026-01-21 11:33:12) View Log
  • ✅ Mathlib branch lean-pr-testing-12058 has successfully built against this PR. (2026-01-22 09:31:54) View Log

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 20, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-20 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. (2026-01-20 10:43:59)
  • ❌ Reference manual branch lean-pr-testing-12058 built against this PR, but generating HTML failed. (2026-01-21 09:46:16) View Log
  • 🟡 Reference manual branch lean-pr-testing-12058 build against this PR didn't complete normally. (2026-01-21 09:48:34) View Log
  • ❌ Reference manual branch lean-pr-testing-12058 built against this PR, but generating HTML failed. (2026-01-21 10:36:10) View Log
  • 🟡 Reference manual branch lean-pr-testing-12058 build against this PR didn't complete normally. (2026-01-21 10:38:26) View Log
  • ❌ Reference manual branch lean-pr-testing-12058 built against this PR, but generating HTML failed. (2026-01-22 08:31:03) View Log
  • 🟡 Reference manual branch lean-pr-testing-12058 build against this PR didn't complete normally. (2026-01-22 08:32:48) View Log

@TwoFX TwoFX changed the title feat: bijection between Char and Fin Char.numCodePoints feat: Fin and Char ranges Jan 21, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 21, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#12058
a4c5dce
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Jan 21, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 21, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#12058
00b86b3
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 21, 2026
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#12058
f4c8688
@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 21, 2026
@leanprover-bot leanprover-bot added the breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. label Jan 21, 2026
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 21, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#12058
e05ddba
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 21, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#12058
1338164
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 21, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#12058
34e04f6
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 21, 2026
@TwoFX TwoFX removed the WIP This is work in progress, and only a PR for the sake of CI or sharing. No review yet. label Jan 21, 2026
@TwoFX TwoFX marked this pull request as ready for review January 21, 2026 11:35
@TwoFX TwoFX requested review from datokrat and kim-em as code owners January 21, 2026 11:36
@TwoFX TwoFX added the changelog-library Library label Jan 21, 2026
datokrat
datokrat approved these changes Jan 21, 2026
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.

Great, thanks! Here are my nitpicks.

@TwoFX TwoFX added this pull request to the merge queue Jan 22, 2026
Merged via the queue into leanprover:master with commit 69b058d Jan 22, 2026
17 checks passed
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 22, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#12058
6768731
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jan 22, 2026
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#12058
4882be8
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Jan 22, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#12058
b8f9f92
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

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

Assignees

No one assigned

Labels

breaks-manual This is not necessarily a blocker for merging, but there needs to be a plan. builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

4 participants

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