I noticed there are no equivalent commands in the Idris-dev GitHub Wiki for Atom's Search (Cntl-Alt-S) and Lift Hole (Cntl-Alt-L) commands in emacs. Does anybody know how to set them?
Whoops, looks like those were called "Attempt solve hole" and "extract hole" on there. I've updated the wiki and put those in the right row. Not sure how we got every editor having different names for these things. I call those "proof search" and "extract lemma". The ide-mode names for these are documented at http://docs.idris-lang.org/en/latest/reference/ide-protocol.html (perhaps we could have that as another column on that wiki?) And you can also see the actual keybindings for those things in the idris-mode source: https://github.com/idris-hackers/idris-mode/blob/2cd2ace9327248e141c35127b8ef9114a1301a1d/idris-keys.el#L54