Go To Definition for Imports

[Kha]

No description provided.

[leodemoura]

and "Go To Definition for notation/macros" :)

[larsk21]

and "Go To Definition for notation/macros" :)

What is the current state of this? I have noticed that "go to definition" already works on notation/macros such as <$> or #[], but not on, for example, <|.

[Kha]

I have noticed that "go to definition" already works on notation/macros such as <$> or #[], but not on, for example, <|.

Go-to for builtins should be covered by #937. <|, however, is an unfortunate special case: since it unfolds to syntax that is made up of "original" tokens only (more specifically, the first and last token are original), the editor instead jumps to elabApp.

[Kha]

The relevant check is at

lean4/src/Lean/Server/InfoUtils.lean

Line 131 in 60a7037

return i.contains hoverPos

, so this affects other users of hoverableInfoAt? as well. A potential fix could be to choose the innermost info node that is not contained in an info node of the same range, but that is not immediately implementable using the current smallestInfo?.