Lan*_*ard 5 emacs coq proof-general coqide
在大多数IDE或文本编辑器中,您可以右键单击一个术语,它会将您带到定义该术语的文件中.CoqIDE似乎没有,所以我一直在做coqdoc myfile.v --html,然后去生成的HTML文档.但该文件中唯一可点击的术语是Coq标准库.由ssreflect定义的术语(例如)不可单击.
有没有一种标准的方法能够在Coq文件中快速查找定义某些术语/标识符(以及它的源代码)的位置？无论是在CoqIDE还是在emacs + ProofGeneral中(我使用的是CoqIDE,但如果emacs/ProofGeneral具备此功能,我会切换).
或者是为每个Coq项目和您使用的依赖项生成文档的标准方法？
如果您突出显示一个术语,并执行查询 - >定位,或者您进行评估Locate some_identifier.,您将获得该常量的全名.如果您知道依赖项的安装位置,这将告诉您在哪里查找标识符.
编辑:如果您想要标识符的定义,您可以Print.如果你只是想要它的类型,你可以使用About,或Check(它也接受表达式,而不仅仅是标识符).
| 归档时间： |
|
| 查看次数： |
245 次 |
| 最近记录： |