Go-to-definition for types in hover

@Kha suggested exploring how go to definition could look like for a type shown in a hover. It seems the front end part of this feature would work quite well, with a few drawbacks.

1. Markdown code blocks ( ```lean) do not support links, so we would need to switch to language independent HTML code blocks (<code>) for the type in the hover (not for the documentation with possible lean code examples).
2. This would require enabling HTML in hovers in the client (with a limited set of allowed tags for security reasons), which is currently only support per MarkdownString, i.e. needs to be set for each incoming hover text. This is supposed to change with LSP 3.17 (see this issue).
3. Although this works in VSCode and other Markdown renderers, I'm not sure if links (of the form []()) are always rendered as such inside HTML code blocks, which might be relevant for other editors or if a renderer is changed.
4. HTML code blocks do not fill the hover completely and have a slightly darker background, which looks a bit weird.

The benefit, of course, is the possibility of jumping to the definition of a type appearing in the type of an expression in the code, which I find quite useful. What do you all think of it?

The issue does not name repository files, tests, or entry points. Start with the listed hover-rendering constraints and the linked LSP 3.17 discussion; done would require an agreed implementation path for type links rather than leaving the open design questions unresolved.