IntelliSense for parameters/expressions

[Splines]

Don't know if this is feasible, but I'd greatly appreciate if one could hover over variables and their data types in the Paperproof view such that we can get IntelliSense as shown in these examples:

[lakesare]

It's feasible, vscode-lean4 extension is doing it, and we can copypaste their code.

I think this UI is worth consideration, I was thinking about doing this when I was creating the Single-Tactic Mode.
However

1. it makes paperproof code a bit more convoluted & harder to support
2. more importantly, it would make the UI more convoluted, and I'm not sure if this functionality frequently needed. I think we hover over types when we're getting accustomed to the project, and, after that, we mainly hover over theorems.