String.toNat? should support underscores as digit separators for consistency with numeric literals

[NicolasRouquette]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

[Clear and concise description of the issue]

Context

Lean's numeric literal syntax supports underscores as digit separators for readability:

def myNumber : Nat := 100_000_000  -- ✅ Works

However, String.toNat? (and String.toInt?) do not support this syntax:

#eval "100_000_000".toNat?  -- Returns `none` ❌
#eval "100000000".toNat?    -- Returns `some 100000000` ✅

This inconsistency creates friction when parsing user input, command-line arguments, environment variables, or configuration files where users reasonably expect the same syntax they use in Lean code.

Steps to Reproduce

1. #eval "100_000_000".toNat?  -- Returns none ❌
2. #eval "100_000_000".toInt? -- Returns none ❌

Expected behavior: [Clear and concise description of what you expect to happen]

1. #eval "100_000_000".toNat?  -- Returns some 100000000` ✅
2. #eval "100_000_000".toInt? -- Returns some 100000000` ✅

Actual behavior: [Clear and concise description of what actually happens]

1. #eval "100_000_000".toNat?  -- Returns none ❌
2. #eval "100_000_000".toInt? -- Returns none ❌

Versions

[Output of #version or #eval Lean.versionString]

"4.27.0-nightly-2025-11-30"

[OS version, if not using live.lean-lang.org.]

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Libraries that parse numeric arguments (like lean4-cli) inherit this limitation since they rely on String.toNat?.

See: https://github.com/leanprover/lean4-cli/blob/f75f4926aff7ba19949e16c19094d7298806b1a6/Cli/Basic.lean#L217

See: https://github.com/leanprover/lean4-cli/blob/f75f4926aff7ba19949e16c19094d7298806b1a6/Cli/Basic.lean#L224

I stumbled on this issue while drafting a PR for this issue:
leanprover/doc-gen4#335