From d4f10bc07e575de14edd08ccbcda55e6dd3fa823 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?bc=C2=B2?= <odanoburu@users.noreply.github.com>
Date: Tue, 5 Dec 2023 10:50:10 +0000
Subject: [PATCH] feat: detail error message about invalid mutual blocks
 (#2949)

To prevent user confusion as in this [Zulip
message](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Matching.20on.20prop/near/341456011)
---
 src/Lean/Elab/Declaration.lean                  |  2 +-
 tests/lean/invalidMutualError.lean              | 17 +++++++++++++++++
 tests/lean/invalidMutualError.lean.expected.out |  1 +
 3 files changed, 19 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/invalidMutualError.lean
 create mode 100644 tests/lean/invalidMutualError.lean.expected.out

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index f1cf91a4fc89..31d7d3d7db9d 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -348,7 +348,7 @@ def elabMutual : CommandElab := fun stx => do
         throwErrorAt bad "invalid 'decreasing_by' in 'mutual' block, it must be used after the 'end' keyword"
     elabMutualDef stx[1].getArgs hints
   else
-    throwError "invalid mutual block"
+    throwError "invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs"
 
 /- leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "]" >> many1 ident -/
 @[builtin_command_elab «attribute»] def elabAttr : CommandElab := fun stx => do
diff --git a/tests/lean/invalidMutualError.lean b/tests/lean/invalidMutualError.lean
new file mode 100644
index 000000000000..a338f9c3effc
--- /dev/null
+++ b/tests/lean/invalidMutualError.lean
@@ -0,0 +1,17 @@
+/-! Test invalid mutual block error message -/
+
+inductive Foo : Type where
+  | foo0 : Nat → Foo
+  | foo1 : Foo → Foo
+  | foo2 : Foo → Foo → Foo
+
+mutual
+
+  inductive Bar1 : Foo → Prop where
+    | mk {f : Foo} : Bar f → Bar1 (.foo1 f)
+
+  def Bar : Foo → Prop
+    | .foo1 f => Bar1 f
+    | _ => True
+
+end
\ No newline at end of file
diff --git a/tests/lean/invalidMutualError.lean.expected.out b/tests/lean/invalidMutualError.lean.expected.out
new file mode 100644
index 000000000000..9f47fc1e0ca8
--- /dev/null
+++ b/tests/lean/invalidMutualError.lean.expected.out
@@ -0,0 +1 @@
+invalidMutualError.lean:8:0-17:3: error: invalid mutual block: either all elements of the block must be inductive declarations, or they must all be definitions/theorems/abbrevs