search

meraymond2 / idris-vscode

Idris front-end for VS Code
MIT License
58 stars 10 forks source link

Is it possible to get hole type with just keyboard, not with mouse hover? #71

Closed lwerdna closed 2 years ago

lwerdna commented 2 years ago

Like the title says, I cannot find the idris.<command> to bind to for the purposes of acquiring the type of a hole. I think the equivalent in atom is ctrl+alt+T.

meraymond2 commented 2 years ago

I had neglected to make type-of a separate command. But I've added it now, it's in 0.0.12, so you'll need to update the extension. I've added that suggested keybinding to the readme as well.

If you're using Idris 2, it's better to use the command idris.typeAt, otherwise for Idris 1 it's idris.typeOf. They both do the same thing, but typeAt is more effective.

meraymond2 commented 2 years ago

Very late update, I know, but I've since learned that you can also trigger the hover behaviour from the keyboard. The default is Ctrl-k, Ctrl-i, and the command is Show Hover.