feat: allow upper case single character identifiers when relaxedAutoI…

…mplicit false (#2277)

* feat: allow upper case single character identifiers when relaxedAutoImplicit false

* update tests

* fix tests

* fix another test

---------

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

src/Lean/Elab/AutoBound.lean

@@ -11,7 +11,7 @@ namespace Lean.Elab
 
 register_builtin_option autoImplicit : Bool := {
     defValue := true
-    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
+    descr    := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only single character followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}."
   }
 
 register_builtin_option relaxedAutoImplicit : Bool := {
@@ -39,7 +39,7 @@ Therefore, we do consider identifier with macro scopes anymore.
 
 def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
   match n with
-  | .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
+  | .str .anonymous s => s.length > 0 && (relaxed || isValidAutoBoundSuffix s)
   | _ => false
 
 def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=

tests/lean/1011.lean

@@ -3,3 +3,7 @@ def f (x : A) := x
 set_option relaxedAutoImplicit false
 
 def g (x : A) := x
+def h (x : AA) := x
+def i (x : A1) := x
+def j (x : A₁) := x
+def k (x : A') := x

tests/lean/1011.lean.expected.out

@@ -1 +1 @@
-1011.lean:5:11-5:12: error: unknown identifier 'A'
+1011.lean:6:11-6:13: error: unknown identifier 'AA'

tests/lean/autoBoundImplicits1.lean

@@ -16,7 +16,7 @@ def mkVec : Vec α 0 := ⟨ #[], rfl ⟩
 def Vec.map (xs : Vec α n) (f : α → β) : Vec β n :=
   ⟨ xs.val.map f, sorry ⟩
 
-/- unbound implicit locals must be greek or lower case letters followed by numerical digits -/
+/- unbound implicit locals must be single characters followed by numerical digits -/
 def Vec.map2 (xs : Vec α size /- error: unknown identifier size -/) (f : α → β) : Vec β n :=
   ⟨ xs.val.map f, sorry ⟩
 

tests/lean/interactive/533.lean.expected.out

@@ -1,7 +1,8 @@
 {"textDocument": {"uri": "file://533.lean"},
  "position": {"line": 2, "character": 10}}
 {"items":
- [{"label": "False",
+ [{"label": "F", "kind": 6, "detail": "Sort ?u"},
+  {"label": "False",
    "kind": 22,
    "documentation":
    {"value":