search

ShinKage / idris2-nvim

Simple configuration and extra tools for NVIM + LSP + Idris2
MIT License
46 stars 8 forks source link

Add 'Type-check name' from the book #29

Closed SlayerOfTheBad closed 5 months ago

SlayerOfTheBad commented 1 year ago

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.

mattpolzin commented 7 months ago

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.

SlayerOfTheBad commented 5 months ago

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.