时间戳

首页 > 解决方案 > Emacs 的搜索/提升孔 Idris 命令

emacs - Emacs 的搜索/提升孔 Idris 命令

问题描述

我注意到Idris-dev GitHub Wiki中没有用于 Emacs 中 Atom 搜索 (Cntl-Alt-S) 和 Lift Hole (Cntl-Alt-L) 命令的等效命令。有人知道如何设置它们吗？

标签： emacsidris

解决方案

哎呀，看起来那些在那里被称为“尝试解决洞”和“提取洞”。我已经更新了 wiki 并将它们放在正确的行中。不知道我们是如何让每个编辑对这些东西有不同的名字的。我称这些为“证明搜索”和“提取引理”。这些的 ide-mode 名称记录在http://docs.idris-lang.org/en/latest/reference/ide-protocol.html（也许我们可以将其作为该 wiki 的另一列？）您可以还可以在 idris-mode 源中查看这些东西的实际键绑定：https ://github.com/idris-hackers/idris-mode/blob/2cd2ace9327248e141c35127b8ef9114a1301a1d/idris-keys.el#L54

推荐阅读