You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Hello,
This is due to Idris2 itself not exposing the type to be consumed by eldoc.
Related source code is https://github.com/idris-lang/Idris2/blob/main/src/Idris/IDEMode/SyntaxHighlight.idr#L61
I tried to uncomment code in TODO but id does not return what is expected (Example for Vect output is :type "{+({arg:813} : $resolved997) -> ({arg:816} : Type) -> Type+}")
and fix is beyond my understanding of Idris. Maybe someone else will be able to pick this :)
When the point is over a name, the echo area shows the name, but not its type.
Instead of showing this:
it only shows this:
All other features of the mode are working, including the
idris2-type-at-point
command. It's only eldoc that's broken.The text was updated successfully, but these errors were encountered: