Я заметил, что в нет эквивалентных команд в Idris-dev GitHub Wiki для команд поиска Atom (Cntl-Alt-S) и Lift Hole (Cntl-Alt-L) в emacs. Кто-нибудь знает, как их установить?
Упс, похоже, там назывались «Попытка решить дыру» и «извлечь дыру». Я обновил вики и поместил их в правильный ряд. Не уверен, как у каждого редактора были разные имена для этих вещей. Я называю это «доказательством поиска» и «извлечением леммы». Имена ide-mode для них задокументированы в http://docs.idris-lang.org/en/latest/reference/ide-protocol.html (возможно, мы могли бы иметь это как другой столбец в этой вики?) И вы также можете увидеть фактические сочетания клавиш для этих вещей в источнике idris-mode : https://github.com/idris-hackers/idris-mode/blob/2cd2ace9327248e141c35127b8ef9114a1301a1d/idris-keys.el#L54