From 8375d00d8c84615868dba4a45ec0df4b720b6af5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 21 Jan 2025 04:51:51 +0100 Subject: [PATCH] =?UTF-8?q?fix:=20allow=20=E2=B1=BC=20in=20identifiers=20(?= =?UTF-8?q?#6679)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR changes the identifier parser to allow for the ⱼ unicode character which was forgotten as it lives by itself in a codeblock with coptic characters. --- 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 629ba768f9..03cb47b39f 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 0000000000..17988b47fb --- /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