From bf809b5298e2d528dd9adc3b23eba854977973ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Fri, 10 Oct 2025 18:06:18 +0200 Subject: [PATCH] chore: change the location of error message for coinductive predicates (#10722) This PR changes where errors are displayed when trying to use `coinductive` keyword when targeting things that do not live in `Prop`. Instead of displaying the error above the first element of the mutual block, it is displayed above the erroneous definition. --------- Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com> --- src/Lean/Elab/MutualInductive.lean | 4 ++-- tests/lean/run/coinductive_syntax.lean | 13 +++++++++++++ 2 files changed, 15 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index ffebba0a31..819ef56e72 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -1049,8 +1049,8 @@ private def mkInductiveDeclCore let view0 := views[0]! let isCoinductive := views.any (·.isCoinductive) if isCoinductive then - unless (←rs.allM (forallTelescopeReducing ·.type fun args body => pure body.isProp)) do - throwErrorAt view0.declId "`coinductive` keyword can only be used to define predicates" + if let some i ← rs.findIdxM? (forallTelescopeReducing ·.type fun _ body => pure !body.isProp) then + throwErrorAt views[i]!.declId "`coinductive` keyword can only be used to define predicates" let allUserLevelNames := rs[0]!.levelNames let isUnsafe := view0.modifiers.isUnsafe let res ← withInductiveLocalDecls rs fun params indFVars => do diff --git a/tests/lean/run/coinductive_syntax.lean b/tests/lean/run/coinductive_syntax.lean index 8c03ca45fe..deaad49790 100644 --- a/tests/lean/run/coinductive_syntax.lean +++ b/tests/lean/run/coinductive_syntax.lean @@ -250,3 +250,16 @@ namespace unsafe_test unsafe coinductive infSeq2 (r : α → α → Prop) : α → Prop where | step : r a b → infSeq2 r b → infSeq2 r a end unsafe_test + +/-- +@ +4:14...20 +error: `coinductive` keyword can only be used to define predicates +-/ +#guard_msgs (positions := true) in +mutual + coinductive wrong1 : Prop where + + coinductive wrong2 where + | zero : wrong2 + | succ : wrong1 → wrong2 +end