coqide

2热度

1回答

如何在coq中证明why3生成的脚本？

我使用frama-C WP并希望调试我的ACSL注释（了解为什么证明者说我“不知道”）。 我有一些绿色或橙色的结果。我打开why3 IDE并查看生成的脚本。然后我从列表中选择一个理论/目标，并能够启动Alt-Ergo或Coq IDE。我想在Coq IDE中使用生成的代码。我看到一些公理定理，然后WP 然后，例如： intros a a_1 i_3 i_2 i_1 i t_2 t_1 t t_8 t

coq frama-c coqide why3 2017-08-26

---

2热度

2回答

Vim插件无法识别现有的Perl支持

我一直在Linux机器上使用CoqIDE plugin for Vim来编辑Coq文件。现在，我想在Windows 8安装它，但，当我尝试源插件，我得到 Your vim doesn't support Perl. Install it before using CoqIDE mode. 这很奇怪，因为我:version清楚地看到包括+perl/dyn。这与我需要的+perl不同吗？ 我听说你

perl vim plugins coqide 2014-07-20

---

1热度

2回答

CoqIDE 8.5默认字体

对不起，这个小问题--- CoqIDE在Coq 8.5中的默认字体是什么？尝试Coq 8.6 w/nix-shell -p coq_8_6 --run coqide改变了我的旧CoqIDE字体（和键绑定）;我想让他们回来，但不记得字体名称。确切的版本（不知道这是否重要）是8.5pl1。可悲的是，重启，甚至nix-env --rollback没有恢复的设置（我的8.5安装瓦特/ nix和nix-sh

fonts version coqide 2017-05-29

---

0热度

1回答

CoqIDE和JAVA

我想检索一个文件的编译结果。 v来自coqide或coqc用java处理，而我有一个自动机的处理，我想在java中构建这个自动机的图形界面。 感谢您的回复。

coq coqide 2014-04-16

---

7热度

2回答

Coq/Proof General中的Agda-like编程？

与Agda不同，Coq倾向于将证据与功能分开。 Coq提供的策略非常适合写作证明，但我想知道是否有方法来复制某些Agda模式功能。 具体来说，我想： 阿格达的?或Haskell的_，在那里我可以省略的部分功能的一些等价，而我写它，（希望）有勒柯克告诉我键入我需要把有 抄送Cr的阿格达模式（物化），等效在那里你填写一个?块具有的功能，它将使新?块所需的参数 当我在做什么一个函数中有一个match，C

coq agda dependent-type proof-general coqide 2017-01-24

---

6热度

1回答

在当前环境中未找到参考“X”

我正在使用CoqIDE完成软件基础本手册中关于Coq的练习。我可以成功编译Basics.v，在我的目录中生成Basics.vo和Basics.glob。当我尝试运行Induction.v时，它可以工作。当我尝试编译它时，它会抱怨大量缺失的引用，如evenb和negb_involutive。如果我将Basics.v内容复制到Induction.v中，它会进行编译，但显然这不是要走的路。 这不是问题C

coq coqide 2016-10-19

---