fix: allow ⱼ in identifiers

src/Init/Meta.lean

@@ -93,7 +93,8 @@ def isLetterLike (c : Char) : Bool :=
 def isSubScriptAlnum (c : Char) : Bool :=
   isNumericSubscript c ||
   (0x2090 ≤ c.val && c.val ≤ 0x209c) ||
-  (0x1d62 ≤ c.val && c.val ≤ 0x1d6a)
+  (0x1d62 ≤ c.val && c.val ≤ 0x1d6a) ||
+  c.val == 0x2c7c
 
 @[inline] def isIdFirst (c : Char) : Bool :=
   c.isAlpha || c = '_' || isLetterLike c

tests/lean/run/subscript_parser.lean

@@ -0,0 +1,18 @@
+-- test that we accept all unicode subscripts
+def fₐ : Nat := 0
+def fₑ : Nat := 0
+def fₕ : Nat := 0
+def fᵢ : Nat := 0
+def fⱼ : Nat := 0
+def fₖ : Nat := 0
+def fₗ : Nat := 0
+def fₘ : Nat := 0
+def fₙ : Nat := 0
+def fₒ : Nat := 0
+def fₚ : Nat := 0
+def fᵣ : Nat := 0
+def fₛ : Nat := 0
+def fₜ : Nat := 0
+def fᵤ : Nat := 0
+def fᵥ : Nat := 0
+def fₓ : Nat := 0