'wrong argument name' error msg should be clickable

Stream: lean4

[Alok Singh]

Consider:

def f (x : Int) := x
-- `invalid argument name 'y' for function 'f'`. `f` should be hoverable/clickable in the infoview

It feels like the definition of f should be clickable, and that would help debug the error. Also, maybe all f's valid argument names should be listed to make it easier to debug?

[Eric Wieser]

This looks like an easy PR, by using {.ofConstName f} in the error message interpolation

[Alok Singh]

what about displaying f's arguments?

[Eric Wieser]

That sounds more bike-sheddy, and probably not one that could be merged as quickly

[Alok Singh]

i know, it's for follow up exploration