Agda符号的Emacs键盘快捷键是什么？

我的意思是列表符号，以防它在标题中显示不好。Agda符号的Emacs键盘快捷键是什么？

这不是像书中所说的\bl。

2016-11-19 Marko Grdinic

你把你的.emacs文件中的“一些额外的Emacs定义”部分的代码？ –

是的，这是我需要的。只有复制/粘贴消耗换行符，所以如果有人以文本而不是pdf提供了定义，那就不会太坏。我会尽力自己找到它。 –

的book提供的代码，以使输入在“一些额外的Emacs定义”补遗简单：

(eval-after-load "quail/latin-ltx" 
    '(mapc (lambda (pair) 
      (quail-defrule (car pair) (cadr pair) "TeX")) 
      '(("\\bb" "") ("\\bl" "") ("\\bs" "") ("\\bt" "") ("\\bv" "") ("\\cv" "⋎") ("\\comp" "○") ("\\m" "↦") ("\\om" "ω"))))

你只需要把它从这里复制并粘贴到你的.emacs文件。

来源

2016-11-19 16:56:12

我应该注意的是，这本书还有一些额外的内容。 –

使用M-x然后agda-input-show-translations获取所有字符绑定的表。然后您可以使用C-s来搜索特定的字符。

来源

2016-11-19 15:33:28

我得到了“失败的我搜索：”为''。 – user3237465

这不是emacs模式的一部分，但我提交了一个Pull Request来添加丢失的黑板粗体字母。

来源

2016-11-20 10:10:09 gallais

在我来说，我刚才输入在Emacs

\bL

，它正确地给了我在黑板加粗字体。这是与Agda 2.5.3（通过在Ubuntu 16.04下的每个官方文档的黑客安装）

来源

2018-03-10 21:09:09 tinlyx

Agda符号的Emacs键盘快捷键是什么？

回答

相关问题