feat(frontends/lean/scanner): allow ' in the beginning of identifiers

src/frontends/lean/scanner.cpp

@@ -435,7 +435,7 @@ void scanner::next_utf(buffer<char> & cs) {
 }
 
 static bool is_id_first(buffer<char> const & cs, unsigned i) {
-    if (std::isalpha(cs[i]) || cs[i] == '_')
+    if (std::isalpha(cs[i]) || cs[i] == '_' || cs[i] == '\'')
         return true;
     unsigned u = utf8_to_unicode(cs.begin() + i, cs.end());
     return is_letter_like_unicode(u);

tests/lean/run/tick_id.lean

@@ -0,0 +1,9 @@
+def id₁ {'a : Type} (x : 'a) : 'a := x
+
+def id₂ {α : Type} (a : α) : α := a
+
+def id₃ {β : Type} (b : β) : β := b
+
+check λ (α β : Type) (f : α → β) (a : α), f a
+
+check λ ('a 'b : Type) (f : 'a → 'b) (a : 'a), f a