From 7ae15ef48d6eb94b4da8168a614bc2a0bc6e03db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 17 Jan 2025 19:15:22 +0100 Subject: [PATCH] =?UTF-8?q?fix:=20allow=20=E2=B1=BC=20in=20identifiers?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Init/Meta.lean | 3 ++- tests/lean/run/subscript_parser.lean | 18 ++++++++++++++++++ 2 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/subscript_parser.lean 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