fix: make @[elab_as_elim] require at least one discriminant (#5671)

This is an oversight in `getElabElimExprInfo`. If there are no
discriminants, then there is no point in elaborating as an eliminator.

src/Lean/Elab/App.lean

@@ -777,7 +777,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do
   forallTelescopeReducing elimType fun xs type => do
     let motive  := type.getAppFn
     let motiveArgs := type.getAppArgs
-    unless motive.isFVar do
+    unless motive.isFVar && motiveArgs.size > 0 do
       throwError "unexpected eliminator resulting type{indentExpr type}"
     let motiveType ← inferType motive
     forallTelescopeReducing motiveType fun motiveParams motiveResultType => do

tests/lean/run/elabAsElim.lean

@@ -193,3 +193,15 @@ In this example, `h0` and `h1` used to be reversed, leading to a kernel typechec
 -/
 example (n : Nat) (h0 : n ≠ 0) (h1 : n ≠ 1) : n - 2 ≠ n - 1 :=
   Nat.recOn n (by simp) (by rintro (_ | _) <;> simp) h0 h1
+
+/-!
+Check that eliminators need at least one discriminant
+-/
+
+/--
+error: unexpected eliminator resulting type
+  p
+-/
+#guard_msgs in
+@[elab_as_elim]
+theorem mySillyEliminator {p : Prop} (h : p) : p := h