From 4614b758e1addd597cab2c9075968206cb7bec35 Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Thu, 10 Oct 2024 10:20:35 -0700
Subject: [PATCH] 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         |  2 +-
 tests/lean/run/elabAsElim.lean | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 1df15e5a4dd3..b8a96c55fd5d 100644
--- a/src/Lean/Elab/App.lean
+++ b/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
diff --git a/tests/lean/run/elabAsElim.lean b/tests/lean/run/elabAsElim.lean
index 2b950aa6e7cf..7814dae89b5e 100644
--- a/tests/lean/run/elabAsElim.lean
+++ b/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