From 1246e7f5de78a38663cdc6ebb7fbad57d9ab5eb8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?bc=C2=B2?= Date: Wed, 22 Nov 2023 10:43:34 -0300 Subject: [PATCH] Detail error message about invalid mutual blocks 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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