Hovering on String.append : String → String → String highlights two out of three String

[kim-em]

The middle String in the signature of "String.append : String → String → String" doesn't have a hover.

[david-christiansen]

Interestingly, it doesn't have the correct hover in the infoview either.

If I write

#check String.append

and then hover the resulting signature, the first and last String are highlighted with their proper docstrings, but the second one only gets String : Type in its tooltip. Go-to-def doesn't work on it either. So this is probably a bug in Lean that needs fixing.

[david-christiansen]

See leanprover/lean4#4972

[david-christiansen]

This was fixed upstream.