From b7ea66d8d3ec3872dcd2906fd04d8ba91a12177b Mon Sep 17 00:00:00 2001
From: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Date: Thu, 16 Oct 2025 15:57:58 +0200
Subject: [PATCH] fix: consider underscores in `getHexNumSize` (#10719)

This PR fixes `getHexNumSize` to consider underscores. Previously, only
the amount of bytes was counted, making it output 9 for `1234_abcd`
instead of the actual number of digits, which is 8.
---
 src/Init/Meta/Defs.lean    | 10 ++++++++--
 tests/lean/run/hexnum.lean |  4 ++++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/Init/Meta/Defs.lean b/src/Init/Meta/Defs.lean
index f0f216a843..e75f4a59a9 100644
--- a/src/Init/Meta/Defs.lean
+++ b/src/Init/Meta/Defs.lean
@@ -1210,10 +1210,16 @@ def getHexNumVal (s : Syntax.HexNum) : Nat :=
   isHexNum? s.raw |>.getD 0
 
 /-- Returns the number of hexadecimal digits. -/
-def getHexNumSize (s : Syntax.HexNum) : Nat :=
+partial def getHexNumSize (s : Syntax.HexNum) : Nat :=
   match Syntax.isLit? hexnumKind s.raw with
-  | some val => val.utf8ByteSize
+  | some val => go val 0 0
   | _        => 0
+where
+  go (s : String) (p : String.Pos.Raw) (n : Nat) : Nat :=
+    if String.Internal.atEnd s p then
+      n
+    else
+      go s (String.Internal.next s p) (if String.Internal.get s p = '_' then n else n + 1)
 
 /--
 Extracts the parsed name from the syntax of an identifier.
diff --git a/tests/lean/run/hexnum.lean b/tests/lean/run/hexnum.lean
index 923d579f54..885a9230c4 100644
--- a/tests/lean/run/hexnum.lean
+++ b/tests/lean/run/hexnum.lean
@@ -22,3 +22,7 @@ macro_rules
 /-- info: (3, 10) : Nat × Nat -/
 #guard_msgs in
 #check #00a
+
+/-- info: (8, 65536) : Nat × Nat -/
+#guard_msgs in
+#check #0001_0000