Show type of hole on hover

[michaelmesser]

This requires stripping the leading ?.

https://github.com/edwinb/idris2-vim/blob/964cebee493c85f75796e4f4e6bbb4ac54e2da9e/ftplugin/idris2.vim#L27-L29

[meraymond2]

Cool, that's an easy fix :+1:

Do you prefer having the premises as well in the hover text, or just the type of the hole itself? For

imap : Vect n a -> Vect n b
imap xs = ?imap_rhs

the full type information it returns

 0 b : Type
 0 a : Type
 0 n : Nat
   xs : Vect n a
-------------------------------------
imap_rhs : Vect n b

but that might get annoying if there's a lot of locals.

[michaelmesser]

I think it would be best to show the locals at least until you can hover over the locals to see the types.

[meraymond2]

This should work now in the latest release.

[michaelmesser]

I can confirm that it works.