search

idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

What about lifting/extracting holes? #79

Closed bentxt closed 7 years ago

bentxt commented 7 years ago

Appearantly you can "Lift a hole to the top level as a new function declaration" (from the Idris Book) with Ctrl-Alt-L in the Atom editor.

The Emacs package seems to have that implemented too:

from https://github.com/idris-hackers/idris-mode: C-c C-e: Extract a hole or provisional definition name to an explicit top level definition.

I could not find this functionality in this package.

bentxt commented 7 years ago

of course I found out right after filing this issue: it is 

<Leader>l 
(IdrisMakeLemma)