search

meraymond2 / idris-vscode

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

Support generate definition #35

Closed michaelmesser closed 3 years ago

michaelmesser commented 3 years ago

Here is how generate definition is defined in Idris 2's vim plugin.

meraymond2 commented 3 years ago

Cool, I didn't know about that command, I'll see about implementing it. I will also look at proof-search-next and generate-definition-next.

meraymond2 commented 3 years ago

https://github.com/meraymond2/idris-vscode/pull/39

This has been released in 0.0.8.