Hovering on inductive types should show their definition

[Alizter]

In #340 there is a basic type showing hover implemented. For inductive types this doesn't work due to how they are stored in the enviornment. In that case, we should experiment with printing the definition of the inductive type (with type annotations).

So hovering over nat should give:

Inductive nat : Set :=  O : nat | S : nat -> nat.

Perhaps formatted a bit nicer like

Inductive nat : Set :=
|  O : nat 
|  S : nat -> nat.

[ejgallego]

Note that I fixed the type printing on hover for inductives, whether to print the definition indeed is open IMHO.

[ejgallego]

Still unsure how to better handle this, many inductives can be huge.

Do you have an idea on what to do? Maybe we could summarize the inductive definition somehow?

I'm unsure if Javascript is allowed in the hover, html is, we could use <details>

[Alizter]

I suppose for now, showing the type is enough. It will let users disambiguate between types and terms at least.

[ejgallego]

I still think this issue has value tho, it is just that it is not clear how to implement it yet.

[ejgallego]

If LSP would get multi-hover that would be nice.

[Alizter]

What we should do instead is use the peek menu and inspect using a goto.

[ejgallego]

That already works fine, right?