diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 629ba768f987..03cb47b39fee 100644 --- a/src/Init/Meta.lean +++ b/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 diff --git a/tests/lean/run/subscript_parser.lean b/tests/lean/run/subscript_parser.lean new file mode 100644 index 000000000000..17988b47fb92 --- /dev/null +++ b/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