diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 7d7181a62..d57ce249e 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -59,14 +59,10 @@ bool is_letter_like_unicode(unsigned u) { (0x1f00 <= u && u <= 0x1ffe) || // Polytonic Greek Extended Character Set (0x2100 <= u && u <= 0x214f); // Letter like block } -bool is_super_sub_script_alnum_unicode(unsigned u) { +bool is_sub_script_alnum_unicode(unsigned u) { return - (0x2070 <= u && u <= 0x2079) || // most (numeric) superscripts (0x207f <= u && u <= 0x2089) || // n superscript and numberic subscripts - (0x2090 <= u && u <= 0x209c) || // letter-like subscripts - u == 0x00B2 || // 2 superscript - u == 0x00B3 || // 3 superscript - u == 0x00B9; // 1 superscript + (0x2090 <= u && u <= 0x209c); // letter-like subscripts } void scanner::next() { @@ -333,7 +329,7 @@ bool is_id_rest(char const * begin, char const * end) { if (std::isalnum(*begin) || *begin == '_' || *begin == '\'') return true; unsigned u = utf8_to_unicode(begin, end); - return is_letter_like_unicode(u) || is_super_sub_script_alnum_unicode(u); + return is_letter_like_unicode(u) || is_sub_script_alnum_unicode(u); } static char const * g_error_key_msg = "unexpected token"; diff --git a/tests/lean/626a.lean b/tests/lean/626a.lean index 475ea9fdf..2791ce8d7 100644 --- a/tests/lean/626a.lean +++ b/tests/lean/626a.lean @@ -1,9 +1,9 @@ namespace foo - definition C¹ := nat - definition foo (c : C¹) := nat.rec_on c _ _ + definition C₁ := nat + definition foo (c : C₁) := nat.rec_on c _ _ end foo namespace boo - notation `C¹` := nat - definition foo (c : C¹) := nat.rec_on c _ _ + notation `C₁` := nat + definition foo (c : C₁) := nat.rec_on c _ _ end boo diff --git a/tests/lean/run/super.lean b/tests/lean/run/super.lean new file mode 100644 index 000000000..0226943fa --- /dev/null +++ b/tests/lean/run/super.lean @@ -0,0 +1,4 @@ +constant f : nat → nat +notation a `²` := f a +variable a : nat +check a²