idris2-nvim icon indicating copy to clipboard operation
idris2-nvim copied to clipboard

Add 'Type-check name' from the book

Open SlayerOfTheBad opened this issue 1 year ago • 1 comments

The book 'Type-driven Development with Idris' by Edwin Brady describes a 'Type-check name' command in the Atom extension for Idris (called with Ctrl-Alt-T).

It is described as showing the type of a hole, and the types of all the variables associated with it.

It seemed useful to me but there wasn't tooling for it, so I have attempted to replicate its functionality as close to the description in the book as I could get it.

SlayerOfTheBad avatar Sep 13 '23 22:09 SlayerOfTheBad

I am pretty sure that what you are describing is what the Idris 2 LSP already surfaces as the result of the hover action.

That is, the Neovim plugin does not need to offer a special option to support it because you can already bind whatever you'd like to vim.lsp.buf.hover. I've got '<Leader>t' bound to hover which gives the same result as you used to get from Edwin's older Neovim plugin and the same result as I am pretty sure Ctrl-Alt-T gave in the Atom extension.

mattpolzin avatar Apr 07 '24 01:04 mattpolzin

Yeah I realized this a couple of weeks after I'd made this pull request, and then forgot I made this PR. I'll close it now, thanks.

SlayerOfTheBad avatar May 25 '24 07:05 SlayerOfTheBad