String.toNat? and String.toInt? handling underscores

Stream: lean4

[Nicolas Rouquette]

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` ✅

I wrote an issue about this here: https://github.com/leanprover/lean4/issues/11538

[Nicolas Rouquette]

I ran into this issue while developing a PR to add support for specifying "max heartbeats" in doc-gen4, see this PR: https://github.com/leanprover/doc-gen4/pull/336

[Kim Morrison]

I've opened a PR to implement this: https://github.com/leanprover/lean4/pull/11541

The implementation adds support for underscores as digit separators in String.toNat?, String.toInt?, and related functions. Underscores cannot appear at the start, end, or consecutively, matching the validation rules for numeric literals.

Examples:

#eval "100_000_000".toNat?  -- some 100000000
#eval "1_000".toInt?        -- some 1000
#eval "-1_000_000".toInt?   -- some (-1000000)

[Nicolas Rouquette]

Thanks @Kim Morrison !