update the name regex too

pygments/lexers/lean.py

@@ -137,6 +137,10 @@ class Lean4Lexer(RegexLexer):
     mimetypes = ['text/x-lean4']
     version_added = '2.18'
 
+    # TODO: update this regex for Lean 4
+    _name = Lean3Lexer._name
+    _name_segment = Lean3Lexer._name_segment
+
     keywords1 = (
         'import', 'abbreviation', 'opaque_hint', 'tactic_hint', 'definition',
         'renaming', 'inline', 'hiding', 'parameter', 'lemma', 'variable',
@@ -163,7 +167,7 @@ class Lean4Lexer(RegexLexer):
     )
 
     operators = (
-        '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!', '`',
+        '!=', '#', '&', '&&', '*', '+', '-', '/', '@', '!',
         '-.', '->', '.', '..', '...', '::', ':>', ';', ';;', '<',
         '<-', '=', '==', '>', '_', '|', '||', '~', '=>', '<=', '>=',
         '/\\', '\\/', '∀', 'Π', 'λ', '↔', '∧', '∨', '≠', '≤', '≥',
@@ -183,9 +187,8 @@ class Lean4Lexer(RegexLexer):
             (words(keywords3, prefix=r'\b', suffix=r'\b'), Keyword.Type),
             (words(operators), Name.Builtin.Pseudo),
             (words(punctuation), Operator),
-            ("[A-Za-z_\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2100-\u214f]"
-             "[A-Za-z_'\u03b1-\u03ba\u03bc-\u03fb\u1f00-\u1ffe\u2070-\u2079"
-             "\u207f-\u2089\u2090-\u209c\u2100-\u214f0-9]*", Name),
+            (_name_segment, Name),
+            (r'``?' + _name, String.Symbol),
             (r'\d+', Number.Integer),
             (r'"', String.Double, 'string'),
             (r'[~?][a-z][\w\']*:', Name.Variable),

tests/examplefiles/lean4/Test.lean

@@ -233,3 +233,8 @@ theorem IsChain.exists_maxChain (hc : IsChain r c) : ∃ M, @IsMaxChain _ r M 
 -- other bits of tricky syntax
 @[to_additive "See note [foo]"]
 lemma mul_one : sorry := sorry
+
+variable {ι A B : Type*} (𝒜 : ι → A) (ℬ : ι → B)
+
+#check `𝒜.a
+#check ``𝒜