chore: cleanup and remove Array.getA

src/Init/Data/Array/Basic.lean

@@ -93,9 +93,6 @@ if h : i < a.size then some (a.get ⟨i, h⟩) else none
 def getD (a : Array α) (i : Nat) (v₀ : α) : α :=
 if h : i < a.size then a.get ⟨i, h⟩ else v₀
 
-def getA [Inhabited α] (a : Array α) (i : Nat) : α :=
-getD a i (arbitrary _)
-
 def getOp [Inhabited α] (self : Array α) (idx : Nat) : α :=
 self.get! idx
 

src/Init/Lean/Elab/Term.lean

@@ -792,18 +792,18 @@ fun stx _ =>
 
 /-- Main loop `getFunBinderIds?` -/
 private partial def getFunBinderIdsAux? : Bool → Syntax → Array Syntax → TermElabM (Option (Array Syntax))
-| false, Syntax.node `Lean.Parser.Term.app args, acc => do
-  (some acc) ← getFunBinderIdsAux? false (args.getA 0) acc | pure none;
-  getFunBinderIdsAux? true (args.getA 1) acc
-| _, Syntax.node `Lean.Parser.Term.id args, acc =>
-  if (args.getA 1).isNone then
-    pure (some (acc.push (args.getA 0)))
-  else
-    pure none
-| _, n@(Syntax.node `Lean.Parser.Term.hole _), acc => do
-  ident ← mkFreshAnonymousIdent n;
-  pure (some (acc.push ident))
-| idOnly, stx, acc => pure none
+| idOnly, stx, acc =>
+  match_syntax stx with
+  | `($f $a) =>
+     if idOnly then pure none
+     else do
+       (some acc) ← getFunBinderIdsAux? false f acc | pure none;
+       getFunBinderIdsAux? true a acc
+  | `(_) => do ident ← mkFreshAnonymousIdent stx; pure (some (acc.push ident))
+  | stx  =>
+    match stx.isSimpleTermId? with
+    | some id => pure (some (acc.push id))
+    | _       => pure none
 
 /--
   Auxiliary functions for converting `Term.app ... (Term.app id_1 id_2) ... id_n` into #[id_1, ..., id_m]`
@@ -825,11 +825,6 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
       pure (binders, newBody)
     };
     match binder with
-    | Syntax.node `Lean.Parser.Term.id args => do
-      unless (args.getA 1).isNone $ throwError binder "invalid binder, simple identifier expected";
-      let ident := args.getA 0;
-      let type  := mkHole;
-      expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident type)
     | Syntax.node `Lean.Parser.Term.hole _ => do
       ident ← mkFreshAnonymousIdent binder;
       let type := binder;
@@ -851,7 +846,13 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
           match idents? with
           | some idents => expandFunBindersAux body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
           | none        => processAsPattern ()
-    | _ => processAsPattern ()
+    | binder =>
+      match binder.isTermId? with
+      | some (ident, extra) => do
+        unless extra.isNone $ throwError binder "invalid binder, simple identifier expected";
+        let type  := mkHole;
+        expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident type)
+      | none => processAsPattern ()
   else
     pure (newBinders, body)
 

src/Init/Lean/Parser/Term.lean

@@ -199,4 +199,22 @@ open Parser
 def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
 args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
 
+def Syntax.isTermId? (stx : Syntax) : Option (Syntax × Syntax) :=
+stx.ifNode
+ (fun node =>
+    if node.getKind == `Lean.Parser.Term.id && node.getNumArgs == 2 then
+      some (node.getArg 0, node.getArg 1)
+    else
+      none)
+ (fun _ => none)
+
+def Syntax.isSimpleTermId? (stx : Syntax) : Option Syntax :=
+stx.ifNode
+ (fun node =>
+    if node.getKind == `Lean.Parser.Term.id && node.getNumArgs == 2 && (node.getArg 1).isNone then
+      some (node.getArg 0)
+    else
+      none)
+ (fun _ => none)
+
 end Lean