Coq/Proof General中是否支持类似Agda的编程方式？
与Agda不同，Coq倾向于将证明与函数分开。Coq提供的策略非常适合编写证明，但我想知道是否有一种方法可以复制一些Agda-mode的功能。 具体来说，我想要： 一些类似于Agda的 ? 或 Haskell 的 _，在编写函数时可以省略部分内容，然后（希望）让Coq告诉我需要放置在那里...
Emacs下Coq/Proof General关键字和运算符的Unicode字形
这个问题涉及到在Emacs中配置Proof General中的Coq模式。我试图让Emacs自动将Coq中的关键词和符号替换为相应的Unicode字符。我成功地将fun定义为希腊小写字母lambda λ，将forall定义为全称量词符号∀等。我已经成功地为单词定义了符号。 问题在于，当我尝试...
无法向OCaml顶层、coqtop（以及Proof General）提供长达1024个字符以上的输入。
编辑4: 原来这只是TTY输入的限制; 没有OCaml、Coq或Emacs导致问题。 我正在使用Emacs中的Proof General编写Coq程序，发现了一个输入太长的错误。如果提交给coqtop的区域通过Proof General包含超过1023个字符，则Proof General...
如何高效地查找 Coq 中标识符的定义位置？
在大多数IDE或文本编辑器中，您可以右键单击术语，然后转到定义该术语的文件。但是CoqIDE似乎没有这个功能，所以我一直在使用coqdoc myfile.v --html，然后转到生成的HTML文档。但是，在该文件中，只有Coq标准库的术语可点击。由ssreflect定义的术语（例如）无法点击...
使用Coq Proof General时，Emacs会在每个周期上执行。我该如何停止它？
我正在Aquamacs中使用Emacs中的Proof General，每次我键入一个句号（“.”），所有内容都会被执行（直到那个句号）。它看起来像是电动行为，但事实并非如此。所有其他按键都表现正常。 我知道这是一种模式，当我意外使用某些键绑定时，它就会启动。如果我重新启动会话，效果将停止，但...