fix: hovers and docstrings for (co)inductive types

[david-christiansen]

This PR fixes a regression introduced by #10307, where hovering the name of an inductive type or constructor in its own declaration didn't show the docstring. In the process, a bug in docstring handling for coinductive types was discovered and also fixed. Tests are added to prevent the regression from repeating in the future.

[david-christiansen]

@wkrozowski Could you please confirm that this is correct?

This line was removing the namespaces from the constructor names. With it, the constructors' docstrings weren't being placed on the correct names and thus didn't appear in hovers anywhere. Additionally, adding the terminfo below led to an error, because the constant that the constructor's declId represents was not present in the environment (because the name had the namespace removed).

Removing this line fixes docstrings for coinductive predicates' constructors more generally, and it also allows the overall fix for in-declaration hovers in this PR to work without error. All tests still pass, but I don't have much of a feel for how good our test coverage is for coinductive predicates.

[wkrozowski]

Tldr; that looks good to me. The updateViewRemovingFunctorName is an artifact from my older attempts, that is not really needed.

In detail, in the case of coinductive predicates inelabInductives we look at the InductiveView and add a _functor postfix to it.

 if isCoinductive then
    runTermElabM fun vars => do
      checkNoInductiveNameConflicts elabs (isCoinductive := true)
      let flatElabs := elabs.map fun e => {e with view := updateViewWithFunctorName e.view}

We elaborate this as a normal inductive, and then use it in for generating the coinductive predicate with the original name. The updateViewRemovingFunctorName was originally doing that. However, if you inspect elabInductives you will observe that elabInductiveViewsPostprocessingCoinductive is called with the original view, so there is no need to remove the postfix.

[david-christiansen]

Thanks! That was how I'd understood it as well, but without deeply understanding this process I wanted you to check before a merge.

Thanks again!

[david-christiansen]

@mhuisi This touches a language server test, so I'll wait for your approval. I don't expect it to be at all controversial, though, as it merely improves test coverage a bit.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3931a72573a896ad57cf23ab6bf3fe1bc90e8680 --onto 705dac4f77aa60d749ee2b37d102518d772d6e53. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-10 20:41:16)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3931a72573a896ad57cf23ab6bf3fe1bc90e8680 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-10 20:41:17)

[wkrozowski]

Could you please remove updateViewRemovingFunctorName from Coinductive.lean before proceeding?

[wkrozowski]

Tldr; that looks good to me. The updateViewRemovingFunctorName is an artifact from my older attempts, that is not really needed.

In detail, in the case of coinductive predicates inelabInductives we look at the InductiveView and add a _functor postfix to it.

 if isCoinductive then
    runTermElabM fun vars => do
      checkNoInductiveNameConflicts elabs (isCoinductive := true)
      let flatElabs := elabs.map fun e => {e with view := updateViewWithFunctorName e.view}

We elaborate this as a normal inductive, and then use it in for generating the coinductive predicate with the original name. The updateViewRemovingFunctorName was originally doing that. However, if you inspect elabInductives you will observe that elabInductiveViewsPostprocessingCoinductive is called with the original view, so there is no need to remove the postfix.

[david-christiansen]

Could you please remove updateViewRemovingFunctorName from Coinductive.lean before proceeding?

Done! Thanks!

[mhuisi]

The test looks good :-)