rfc: on hover, show the type before the error

Stream: lean4

[Kenny Lau]

When there is an error, when you hover over it, the error is showed before the information related to the declaration, which sometimes makes it more annoying to diagnose and fix the error. I think it's enough that the error is displayed on the right hand side, so on the hover window maybe we can show the type first?

image.png

axiom foo1 : Nat → Int
axiom foo2 : Nat → Nat
example bar : foo2 (foo1 1) = 0 :=

[Marc Huisinga]

#lean4 > [Mouseover pop-up] show type above error @ 💬

[Kenny Lau]

hmm, that's quite unfortunate