From 2a9ba9f795a3085ea171f72ce838debca4e4666c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Sep 2021 19:21:49 -0700
Subject: [PATCH] fix: add support for hierachical names containing numerical
 parts

closes #677
---
 src/Init/Meta.lean      | 15 +++++++++++++--
 tests/lean/run/677.lean | 10 ++++++++++
 2 files changed, 23 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/677.lean

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index e6ec555a50..4736c65ea9 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -636,6 +636,9 @@ private partial def splitNameLitAux (ss : Substring) (acc : List Substring) : Li
     else if isIdFirst curr then
       let idPart := ss.takeWhile isIdRest
       splitRest (ss.extract idPart.bsize ss.bsize) (idPart :: acc)
+    else if curr.isDigit then
+      let idPart := ss.takeWhile Char.isDigit
+      splitRest (ss.extract idPart.bsize ss.bsize) (idPart :: acc)
     else
       []
 
@@ -650,8 +653,16 @@ def decodeNameLit (s : String) : Option Name :=
     | [] => none
     | comps => some <| comps.foldr (init := Name.anonymous)
       fun comp n =>
-        let comp := if isIdBeginEscape comp.front then comp.drop 1 |>.dropRight 1 else comp
-        Name.mkStr n comp.toString
+        let comp := comp.toString
+        if isIdBeginEscape comp.front then
+          Name.mkStr n (comp.drop 1 |>.dropRight 1)
+        else if comp.front.isDigit then
+          if let some k := decodeNatLitVal? comp then
+            Name.mkNum n k
+          else
+            unreachable!
+        else
+          Name.mkStr n comp
   else
     none
 
diff --git a/tests/lean/run/677.lean b/tests/lean/run/677.lean
new file mode 100644
index 0000000000..46302b5cea
--- /dev/null
+++ b/tests/lean/run/677.lean
@@ -0,0 +1,10 @@
+import Lean
+open Lean
+
+def encodeDecode [ToJson α] [FromJson α] (x : α) : Except String α := do
+  let json ← toJson x
+  fromJson? json
+
+#eval IO.ofExcept <| encodeDecode (Name.mkNum Name.anonymous 5)
+
+#eval IO.ofExcept <| encodeDecode (Name.mkStr `bla "foo.boo")