feat: support underscores in String.toNat? and String.toInt? #11541
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This PR adds support for underscores as digit separators in String.toNat?, String.toInt?, and related parsing functions. This makes the string parsing functions consistent with Lean's numeric literal syntax, which already supports underscores for readability (e.g., 100_000_000). The implementation validates that underscores: - Cannot appear at the start or end of the number - Cannot appear consecutively - Are ignored when calculating the numeric value This resolves a common source of friction when parsing user input from command-line arguments, environment variables, or configuration files, where users naturally expect to use the same numeric syntax they use in source code. Closes #11538 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Sonnet 4.5 <[email protected]>
The `lastCharWasDigit` parameter in the fold lambda was not used in the function body, only tracked in the result tuple. Mark it as unused with an underscore prefix to satisfy the linter. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude Sonnet 4.5 <[email protected]>
github-actions
bot
added
the
toolchain-available
Collaborator
|
Mathlib CI status (docs):
|
Collaborator
|
Reference manual CI status:
|
NicolasRouquette
added a commit
to NicolasRouquette/doc-gen4
that referenced
this pull request
Dec 8, 2025
- Removed the parseNatWithUnderscores function and its doc comments with issue references - Simplified getMaxHeartbeats to use flag.as! Nat directly for the CLI flag and s.toNat? for the environment variable - Changed the max-heartbeats flag type from String to Nat in both singleCmd and genCoreCmd - Removed the "Supports underscores as separators" mention from flag descriptions In README.md: - Removed the "Underscores can be used as separators for readability" sentence (the examples still show underscores since they will work in a version of Lean4 that includes this merged PR: leanprover/lean4#11541
algebraic-dev
pushed a commit
that referenced
this pull request
Dec 8, 2025
This PR adds support for underscores as digit separators in String.toNat?, String.toInt?, and related parsing functions. This makes the string parsing functions consistent with Lean's numeric literal syntax, which already supports underscores for readability (e.g., 100_000_000). The implementation validates that underscores: - Cannot appear at the start or end of the number - Cannot appear consecutively - Are ignored when calculating the numeric value This resolves a common source of friction when parsing user input from command-line arguments, environment variables, or configuration files, where users naturally expect to use the same numeric syntax they use in source code. ## Examples Before: ```lean #eval "100_000_000".toNat? -- none ``` After: ```lean #eval "100_000_000".toNat? -- some 100000000 #eval "1_000".toInt? -- some 1000 #eval "-1_000_000".toInt? -- some (-1000000) ``` ## Testing Added comprehensive tests in `tests/lean/run/string_toNat_underscores.lean` covering: - Basic underscore support - Edge cases (leading/trailing/consecutive underscores) - Both `toNat?` and `toInt?` functions - String, Slice, and Substring types All existing tests continue to pass. Closes #11538 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Sonnet 4.5 <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR adds support for underscores as digit separators in String.toNat?, String.toInt?, and related parsing functions. This makes the string parsing functions consistent with Lean's numeric literal syntax, which already supports underscores for readability (e.g., 100_000_000).
The implementation validates that underscores:
This resolves a common source of friction when parsing user input from command-line arguments, environment variables, or configuration files, where users naturally expect to use the same numeric syntax they use in source code.
Examples
Before:
After:
Testing
Added comprehensive tests in
tests/lean/run/string_toNat_underscores.leancovering:toNat?andtoInt?functionsAll existing tests continue to pass.
Closes #11538
🤖 Prepared with Claude Code