Jump to definition of notation

Stream: lean4

[Patrick Massot]

In #check (· + ·) I wasn't able to find a cursor position where jumping to definition leads anywhere but the line @[builtinMacro Lean.Parser.Term.paren] def expandParen : Macro which doesn't seem very useful.

[Mario Carneiro]

There seems to be a bug in the ()-with-· elaborator which causes it to block all hovers from internal nodes

[Gabriel Ebner]

Is this something new? I've also noticed this recently:

example : Inhabited Nat := ⟨Nat.zero⟩
-- hover is always broken on Nat.zero
-- go-to-def is (sometimes?!?) broken on Nat.zero

[Sebastian Ullrich]

Gabriel Ebner said:

Is this something new? I've also noticed this recently:

example : Inhabited Nat := ⟨Nat.zero⟩
-- hover is always broken on Nat.zero
-- go-to-def is (sometimes?!?) broken on Nat.zero

This is a regression from the canonical info introduction, https://github.com/leanprover/lean4/pull/1753

[Sebastian Ullrich]

Patrick's issue is not directly related (and never worked, I assume), but I pushed a fix to the same PR