coq命令的实现

文章/答案/技术大牛

发布

1回答

coq

我在小于或等于的情况下使用析构命令，在小于的情况下使用相同的命令。我在应用( ltb_correct ) command.Error时遇到问题，消息是“找不到此命令。

浏览 14提问于2020-05-13得票数 0

1回答

Dockerfile中所需的冗余eval $(opam env)

bash、docker、dockerfile、coq、opam

#RUN opam pin add coqeval $(opam env)root@3055f16a1d78:/# coqc --version The Coq

浏览 5提问于2022-06-11得票数 1

回答已采纳

1回答

警告:在coq中“从IDE菜单中设置此选项”

coq、coq-tactic、coqide

我正在学习软件基础的"Imp“一章。我在Coq中运行了命令Unset Printing Coercions.，coq消息警告我"Set this option from the IDE menu instead"和命令显然不起作用。我猜这个命令可能在Coq提示环境中可以工作，但是如果我想在Coq中使用"Unset Printing“命令，我想知道我应该做什么？

浏览 7提问于2022-03-15得票数 0

回答已采纳

1回答

通过两种实现对阶乘程序的Coq验证

functional-programming、coq、verification

我是coq的新手，我正在尝试验证factorial程序的功能。这里是“一阶逻辑”中的FOL标准。然而，令我惊讶的是，在用factorial验证coq程序时，常见的方法是定义以下两个函数fact和fact_trmatch n with | 0

浏览 0提问于2018-03-25得票数 2

回答已采纳

1回答

我有一个包含许多文件的Coq项目(比如x1.v，x2.v，...包括一个Makefile，存储在文件夹"C:\Users\WK\Desktop\Personal\ Coq -project“中，并且已经在我的Windows 7机器上安装了Coq 8.3的"C:\Coq”。Coq程序(文件)相互依赖。如何在Coq中执行单个程序(比如x1.v)？我想在Coq中打开一个文件，并逐行编译以了解它，但它给出

浏览 6提问于2012-11-09得票数 2

1回答

在cygwin中安装frama-c时出错

frama-c

Preparing Wp-Coq SourcesMakefile:49: recipe for target

浏览 1提问于2013-06-05得票数 0

2回答

读取系统()命令错误响应消息

c++、compiler-errors、system、command-prompt

我试图在我的Windows10机器上使用C++ system()命令执行一个应用程序(Coq编译器)。这是我的代码：如果afile.v中存在语法/类型错误，Coq将返回有意义的错误消息。目前，即使Coq返回一个错误(我在text.txt应用程序的</e

浏览 0提问于2018-05-15得票数 1

1回答

为什么从根开始时我的容器看起来是空的？

docker、opam

当我进入我的容器时，似乎没有安装任何东西？？docker pull brandojazz/iit-term-synthesis:test。+ '.' + coq_serapi_pin# ['opam', 'repo', '--all-switches&#

浏览 11提问于2022-09-15得票数 0

1回答

如何编译Coq文件的证明通用+ Emacs？

coq

现在，我已经从软件基金会( Software )开始工作了，那里的一切都是放在盘子里的，我很难弄清楚如何建立自己的项目。hello.vcoq_makefile -o Makefile.coq -f _CoqProject这会编译项目，但我无法让make hello只使用这个，并且证明General在编译单个文件时碰巧使用了

浏览 1提问于2019-08-18得票数 2

回答已采纳

3回答

在vim中使用merlin在ocaml中开发coq插件

vim、ocaml、coq、ocamlfind、merlin

我安装了Coq与opam，并想做一个Coq插件。我成功地使用coq_makefile编译了一些插件示例，但是如果我能够在vim中使用merlin来获得类型信息和Coq库的完成，那就太好了。我是否可以将Coq库添加到ocamlfind中？

浏览 9提问于2015-04-14得票数 5

回答已采纳

2回答

如何从外部软件调用抗验证Coq

coq

如何从外部软件中调用验证助理Coq？Coq有API吗？Coq命令行接口是否足够丰富，足以在文件中传递参数并在文件中接收响应？我对Java或C++桥感兴趣。这是一个合理的问题。Coq并不是人们可以期望开发人员友好的API的通常业务软件。我对伊莎贝尔/霍尔也有类似的问题，这是合法的问题，有着不平凡的答案。

浏览 6提问于2017-09-04得票数 9

回答已采纳

2回答

Coqtop无法加载文件

coq

简而言之，我得到了错误的Error: Cannot find a physical path bound to logical path matching suffix <> and prefix LFLFBasics.v包含命令coq_makefile -f _CoqProject *.v -o Makefile生成的第一个chapterMakefile的代码现在我打开coqtop，尝试运行命令From LF R

浏览 1提问于2020-03-03得票数 0

回答已采纳

2回答

Coq的解析器是如何实现的？

parsing、coq

Coq的解析器是如何实现的，我对此感到非常惊讶。例如：对于这种解析器在理论上是如何可行的，有什么建议吗？它应该如何工作？任何材料或知识都是有用的。我只是试着了解这类解析器的一般情况。谢谢。请不要让我自己

浏览 2提问于2017-04-03得票数 10

回答已采纳

1回答

打印Coq术语的内部表示法

ocaml、coq

如何打印Coq中术语的内部OCaml表示(公开数据构造器，如Lambda，App，Rel等……)?

浏览 0提问于2014-03-08得票数 2

1回答

Coq + Emacs？`‘Emacs`’看不到源文件中定义的内容。

emacs、coq

因此，我正在使用Coq使用Emacs作为IDE。proof-general和company-coq都已正确安装和加载。然后我在上面运行coq-Check并得到：错误:在当前环境中找不到参考地址not。但是，例如，Inductive unit : Set := tt.运行得非常好。

浏览 2提问于2021-07-21得票数 1

回答已采纳

1回答

Coq "Error:在使用“参数”命令时没有焦点证明“

compiler-errors、arguments、coq、proof

当我试图在Poly.v文件(章节的源代码，在中可用)上运行Coq时，它会停在上面的一行，给出错误：我认为“证明编辑模式”指的是用策略证明定理的上下文。我不认为它是在这种模式，也不是Coq，因为它说“没有证据编辑正在进

浏览 5提问于2013-11-18得票数 2

回答已采纳

1回答

配置OPAM开关以安装Coq软件包

coq、opam

如果我使用OPAM的全部是Coq包，我应该使用什么作为我的开关？

浏览 0提问于2020-06-29得票数 2

回答已采纳

1回答

coq 8.11.0与ocaml 4.10不相容？

ocaml、coq、opam

我正在使用opam 安装coq，并收到了错误消息。base of this switch (use '--unlock-base' to force)opam switch create with-coq4.05.0对于添加的上下文，我现在使用opam 2.

浏览 0提问于2020-04-04得票数 2

回答已采纳

1回答

Coq命令需要Import做什么？

coq、coq-tactic、coq-extraction

--我不知道它是干什么的，也不知道Ltac模块在哪里。我找到了一个文件plugins/ltac/Ltac.v，但是这个文件不可能是空的，因为这个文件是空的(顺便问一下，包含一个空文件的目的是什么？)Ltac模块是做什么的，Ltac.v文件在哪里，为什么Loacte命令在这种情况下不能工作？谢谢!

浏览 2提问于2018-03-30得票数 4

回答已采纳

1回答

使用OPAM为Coq安装软件包

coq、opam

我正在尝试安装一个coq-contrib包OPAM。我仍然是OPAM和Coq的新手。我使用的是OPAM 1.2.2，得到的结果是：Your request can't be satisfied:即使我在跑步的时候能看到它 opam search <

浏览 4提问于2018-04-02得票数 0

点击加载更多