meraymond2/idris-vscode

Support generate definition

michaelmesser opened this issue · 2 comments

michaelmesser commented

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

meraymond2 commented

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

#39

This has been released in 0.0.8.

  • 👍1