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