找不到Coq库：`错误:无法找到库Floats.`
Coq是一种交互式定理证明工具，用于形式化验证和证明数学定理。在使用Coq进行开发时，有时会遇到找不到库的错误，比如错误信息中提到的无法找到库Floats。
错误信息中的库Floats是Coq中的一个标准库，用于处理浮点数。如果出现找不到库Floats的错误，可能是因为Coq的安装不完整或者库文件没有正确配置。
解决这个问题的方法是检查Coq的安装和配置。首先，确保Coq的版本是最新的，并且已经正确安装。可以通过访问Coq的官方网站（https://coq.inria.fr/）来获取最新版本的Coq。
如果Coq已经正确安装，但仍然找不到库Floats，可以尝试重新安装Coq，并确保在安装过程中选择了包括Floats库的选项。另外，还可以尝试更新Coq的库索引，以确保所有库文件都是最新的。
如果以上方法都无法解决问题，可以尝试在Coq的社区论坛或邮件列表中寻求帮助。Coq的社区非常活跃，有很多经验丰富的开发者可以提供帮助和解答疑问。
总结起来，当出现找不到Coq库Floats的错误时，可以通过以下步骤来解决问题：
- 确保Coq的版本是最新的，并已正确安装。
- 检查Coq的安装配置，确保库文件正确配置。
- 尝试重新安装Coq，并选择包括Floats库的选项。
- 更新Coq的库索引，确保所有库文件都是最新的。
- 寻求Coq的社区帮助，寻找解决方案。
腾讯云相关产品和产品介绍链接地址：
- 腾讯云云服务器（Elastic Cloud Server，ECS）：https://cloud.tencent.com/product/cvm
- 腾讯云对象存储（Cloud Object Storage，COS）：https://cloud.tencent.com/product/cos
- 腾讯云人工智能（AI）：https://cloud.tencent.com/product/ai
- 腾讯云物联网（IoT）：https://cloud.tencent.com/product/iotexplorer
- 腾讯云区块链（Blockchain）：https://cloud.tencent.com/product/baas
- 腾讯云音视频处理（VOD）：https://cloud.tencent.com/product/vod
相关·内容
1回答
Coq正在使用类似于OCaml的模块系统。在OCaml中，我们可以应用像Module_A.Module_B.Func这样的函数，并使用Module_A.Module_B来查找到Func的路径。
然而，我不能在Coq中做类似的事情。例如，如果我只运行Print Coq.Arith.Minus.minus_n_O.，Coq报告Coq.Arith.Minus.minus_n_O is not a defined object.
我必须先加载库，然后才能打印对象。在下面的例子中，它是成功的。
From Coq Require Export Arith.Minus.
Print Coq.Arith.Mi
浏览 6提问于2022-11-19得票数 0
回答已采纳
我对coq很陌生，我试图使用ZArith.Int中的"int“类型，但是coq找不到它。
Require Export ZArith Int.
Open Scope Int_scope.
当我在定义(. -> int -> .)中使用"int“时，coq找不到它。如何将它与库的操作一起正确加载？
浏览 0提问于2014-05-04得票数 1
回答已采纳
Coq 8.7集成了流行的Ssreflect库。因此，可以通过以下方式导入它的库：
From Coq Require Import ssreflect ssrfun ssrbool.
但是，当我尝试导入时，它会报告它是Unable to locate library ssrnat with prefix Coq，并且我在磁盘上的Coq发行版中也找不到ssrnat。是否出于某种原因，ssrnat故意不包含在另一个模块中，或者是我的安装有问题？
浏览 14提问于2017-12-16得票数 2
回答已采纳
这句话在我看来是显而易见的，除非我忽略了一些反例，但我在Coq库中找不到任何这样做的东西。有这样的命令吗？
浏览 0提问于2018-11-10得票数 1
回答已采纳
我正在尝试使用这个库中的引理eqb_sym：https://coq.inria.fr/library/Coq.Structures.Equalities.html 我尝试了“需要导入Coq.Structures.Equalities”。和“要求导入BoolEqualityFacts”，但这两个都不让我使用引理eqb_sym。Coq抱怨它在当前环境中找不到引理。通常，当我在https://coq.inria.fr/library/的库中找到我想要使用的引理时，我在哪里找到要导入的正确模块，以及“是否需要导入模块名称”是正确的使用方法？
浏览 23提问于2019-03-07得票数 2
回答已采纳
我刚刚从CMU讲座中了解到，虽然Check Type以Coq格式返回Type : Type，但左、右的Types被不同的数字隐式索引，因为如果它们是相同的，就会导致类似Burali-Forti悖论的类型理论模拟。如果您试图实现这样一个悖论，Coq将拒绝编译。
我很好奇Coq脚本中这个悖论是什么样子，但是找不到任何代码。一些讨论提到了B.Barras的“coq中的Burali-Forti悖论的形式化”，但是与它的联系被打破了。这一悖论是否有Coq实现？
浏览 2提问于2015-08-13得票数 2
回答已采纳
当我在下面运行Coq脚本时(对原始脚本的简化)：
Inductive w (g: nat): nat -> Prop:=
| z: w g 0.
Lemma x:
forall (i j: nat), w i j -> (forall k: nat, k <= k).
Proof.
Admitted.
Lemma y:
forall (m n: nat),
w m n -> w m n.
Proof.
intros m n H.
apply x in H.
在最后一行中，我得到以下错误消息：
错误:找不到变量k的实例。
有人能向我解释
浏览 2提问于2014-06-25得票数 0
回答已采纳
1回答
我一直在使用上的下载链接来安装Coq。但是，当我在终端或命令提示符上尝试coqc或coqtop时，我收到错误消息，指出找不到该命令。尽管如此，我仍然可以在Coq IDE上很好地运行Coq，但是当我编译buffer时，特别是来自的练习，我得到了以下消息。
Running: coqc -I '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500' '/Users/zhangsheng/Desktop/G/repos/Coqy/cis500/Basics.v' 2>&1
据我所知，2>&1似乎是某种形式
浏览 17提问于2017-01-26得票数 2
回答已采纳
我正在测试AAC战术库，以重写模块的结合性和交换性。根据，人们应该：
根据安装情况，可以修改以下两行，或者将它们添加到.coqrc文件中，替换“”。使用aac_tactics库的路径。
Add Rec LoadPath "." as AAC_tactics.
Add ML Path ".".
Require Import AAC.
Require Instances.
但我不知道如何找到通往aac_tactics库的路径，并使用“。没起作用。
我在Ubuntu 16.04 LTS下安装了Coq，大致如下：
opam repo add coq-releas
浏览 3提问于2016-06-24得票数 1
回答已采纳
我正在遵循一个coq教程，它需要一个基本的coq OPAM库coq:io:system。但我在使用OPAM时遇到了错误。(这是Ubuntu14.04，coq 8.4pl6和opam1.2.1)
我用谷歌搜索了一下，没有找到任何解决方案。
有没有人知道问题可能是什么以及如何修复这个错误？
谢谢。
=-=- Processing actions -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
∗ installed coq:function-ninjas.1.0.0
∗ installed coq:error-handlers.
浏览 1提问于2015-05-26得票数 1
1回答
我正在尝试用涉及字符串的自定义类型来生成ssreflect 。我假设在some中有一些内置的命令类型，但是我在任何地方都找不到它。我在Coq的标准库中看到了一个，但是我不知道这个定义是否会转移到ssreflect库。与Coq标准库相比，我更愿意使用ssreflect。有人能指点我去哪找吗？谢谢。
浏览 11提问于2020-08-14得票数 3
回答已采纳
1回答
我想证明对于任何自然数，n+1都大于0。
定义我自己的大于函数，这样可以很好地工作：
Fixpoint my_gt (n : nat) (m : nat) : bool
:= match n with
| O => false
| S n' => match m with
| O => true
| S m' => my_gt n' m'
end
end.
Lemma GT1: forall n, my
浏览 4提问于2014-04-25得票数 0
我正在尝试编写一个ocamlbuild (myocamlbuild.ml)，它将使用来自另一个文件的定义。我有很多定义，我想要在几个构建插件中使用，我想把它们放在自己的文件中。我试着运行ocamlbuild两次，一次用-没有插件只是为了构建插件。
ocamlbuild -no-plugin myocamlbuild.cmo
然后再来一次
ocamlbuild actual-targets.otarget
但是当我运行第二个插件时，它尝试重新构建插件，并抱怨它找不到包含的库(尽管它存在于_build目录中)。那么，我是否可以说服ocamlbuild在命令行中包含'-I _build _b
浏览 2提问于2013-12-10得票数 4
回答已采纳
因此，我正在使用Coq使用Emacs作为IDE。proof-general和company-coq都已正确安装和加载。
然后打开虚拟whatever_name.v文件并使用Fixpoint关键字定义递归函数。
然后我在上面运行coq-Check并得到：
检查addnm。
错误:在当前环境中找不到参考地址not。
但是，例如，Inductive unit : Set := tt.运行得非常好。
我做错了什么？
浏览 2提问于2021-07-21得票数 1
回答已采纳
我正在使用：
$ coqtop -v
The Coq Proof Assistant, version 8.4pl5 (February 2015)
compiled on Feb 06 2015 17:44:41 with OCaml 4.02.1
我定义了以下CoInductive类型，stream
$ coqtop
Welcome to Coq 8.4pl5 (February 2015)
Coq < CoInductive stream (A : Type) : Type :=
Coq < | Cons : A -> stream A -> stream A
浏览 2提问于2015-05-04得票数 3
回答已采纳
2回答
考虑以下几行( Coq)：
Variable A : Type.
Variable f g : A -> A.
Axiom Hfg : forall x, f x = g x.
Variable a b : A.
Axiom t : g a = g b.
Goal f a = g b.
战术refine (eq_trans (Hfg _) t)解决了目标。也就是说，Coq可以在不需要帮助的情况下用a替换这个孔。但是战术refine (eq_trans (Hfg a) _)用g a = g b代替了上面的目标。
但是，Coq无法单独找到t。战术refine (eq_trans (Hfg
浏览 2提问于2015-02-12得票数 3
回答已采纳
2回答
在coq中使用哪个向量库？
、、、、
我想知道，在coq中是否有一个常用的向量库，即按其类型的长度索引的列表。
有些教程引用了Bvector，但是当我试图导入它时却找不到它。
有Coq.Vectors.Vectordef，但是定义的类型是t，这让我觉得它是为内部使用的。
对于那些不想使用自己的库的人来说，什么是最好的或最常见的做法？标准库中的向量我错了吗？还是我又错过了另一个自由战士？还是人们只是使用列表，并与其长度的证据一起使用？
浏览 10提问于2017-02-17得票数 6
回答已采纳
我想要证明lt n m -> le n m，因为它不存在于Coq的标准库中。
虽然在Coq.Init.Peano中，lt m n被定义为S m <= n，但我无法在假设中使用这种定义。
为什么展开不起作用？似乎只有inversion可以工作。
浏览 0提问于2015-07-21得票数 1
2回答
相同的Linux命令在一个环境中成功，而在另一个环境中失败：
$ coqtop -lv test.v -I Lib
我正在遭受的失败是Debian拉伸和Coq v8.5
$ uname -a
Linux front 4.8.0-1-amd64 #1 SMP Debian 4.8.7-1 (2016-11-13) x86_64 GNU/Linux
$ coqtop -v
The Coq Proof Assistant, version 8.5 (June 2016)
compiled on Jun 9 2016 12:4:46 with OCaml 4.02.3
我得到的错误信息是：
Welc
浏览 3提问于2016-12-04得票数 2
回答已采纳
0回答
我可以使用nix-env -qa [package]查询可用的包，但是我如何查找依赖于主包并且可以单独加载或安装的可选包(例如，库)？示例: Coq (coq-8.6)有包coqPackages_8_6.ssreflect和coqPackages_8_6.mathcomp，我在Nix AFAIK中无法获得有关它们的信息
浏览 11提问于2017-06-15得票数 4
回答已采纳
有人知道在Coq的标准库中有下列定理的证明吗？如果有，我就找不到了。
对于a b c: nat，b >= c -> a+b-c=a+ (b - c)
提前谢谢马库斯。
浏览 2提问于2014-07-07得票数 0
回答已采纳
我试图在Coq中使用更大的数字，而在Coq中，内置Nat类型是不合适的。所以我试图用正型或N型来建立特定的值。
根据BinNums的标准库文档：
正数也将用十进制表示法表示；例如，6%的正数将缩写为xO (xI xH)，N中的数字也将用小数表示法表示；例如，6%的N将缩写Npos (xO (xI xH))。
但我的Coq代码仍在给我Nat输入的数字：
From Coq
Require Import BinNums.
Definition sixp := 6%positive.
Definition sixn := 6%N.
Check sixp.
Check sixn.
结果：
s
浏览 5提问于2020-12-02得票数 2
回答已采纳
1回答
我编写了一个解析器程序(用OCaml编写)，将输入作为xsd，然后将其生成为Coq文件。但在终端机上需要大量的时间(~：0m.0152)才能产生。我想知道一些建议，才能使推车跑得更快？例如，使程序变慢的原因是什么？这是我第一次面对这个运行时间问题。因此，我非常感谢您对此有任何建议/经验？
非常感谢
编辑:我可以尝试通过主文件解释：
open Libxml;; (*it is the library for xml file*)
open Error;; (* it is for the error message*)
let main () =
let xml = parse_
浏览 5提问于2013-10-21得票数 1
回答已采纳
我正在读的书。在中，有一个关于“隐式参数”的部分。在本节中，有一行：
Arguments nil {X}.
当我试图在Poly.v文件(章节的源代码，在中可用)上运行Coq时，它会停在上面的一行，给出错误：
Error: No focused proof (No proof-editing in progress).
我已经将Poly.v文件简化为以下内容，这仍然会导致相同的错误：
Inductive list (X:Type) : Type :=
| nil : list X.
Arguments nil {X}.
在这个错误的中，我唯一能找到的就是
当有人试图从校对编辑模式中使用一
浏览 5提问于2013-11-18得票数 2
回答已采纳
我试图使用液态模板显示0.733675715的数值。
以下代码
{%- assign rate = 0.733675715 -%}
{{ rate }}
结果：0.7336757
我找不到办法：
将数值转换为字符串强制液体以显示所有十进制位
-编辑
注意事项：Azure逻辑应用程序集成帐户使用DotLiquid在JSON/XML/Text之间进行转换
浏览 2提问于2019-10-29得票数 0
我试图定义一个新的表示法范围，并在Coq中添加表示法。我正在遵循Coq手册()中这个页面的指导。
我定义了我的新范围
Declare Scope myHoTT_scope.
Delimit Scope myHoTT_scope with my.
稍后，我想将"*“作为infix操作符添加到作用域中。我做这件事
Infix "*" := concat (at level 40 , left associativity) : myHoTT_scope.
其中，concat是一个已经定义的函数。Coq接受所有这些。它不会引发错误或警告。但是，如果我跑
Locate "
浏览 13提问于2022-01-29得票数 1
回答已采纳
我有档案：
从String0.ml提取的String.v (它来自Coq library)String.ml：是Ocaml 的字符串库)
在将测试文件从Coq解压缩到Ocaml之后，我希望在Ocaml库中使用String.ml，因此我编写了一个替换命令，将所有String0替换为String。
问题是在文件test.v中，我使用了一个定义：
Definition beq_string := beq_dec string_dec.
函数string_dec不在Ocaml库中，而是出现在Coq的字符串库中。
所以当我编译test.ml时有一个错误
open String
let beq_strin
浏览 5提问于2012-04-10得票数 4
回答已采纳
2回答
我试图在Coq中定义一个幂函数，但我似乎找不到要导入的相关模块：
Require Import Coq.Numbers.NatInt.NZPow.
Definition func (a b : nat) : nat := a+b*2^a.
给出以下错误：
Unknown interpretation for notation "_ ^ _".
我有点困惑，因为在中，我看到了以下描述：
幂函数的接口，然后它对自然的规范
此外，这也是：
Module Type PowNotation (A : Typ)(Import B : Pow A).
Infix "^
浏览 2提问于2020-05-08得票数 3
回答已采纳
如何使用在给定库中验证的结果？例如，我希望从库Lemma peano_ind中使用BinInt。我用CoqIDE写这篇文章：
Require Import BinInt.
Check peano_ind.
并获得一个“在当前环境中找不到引用peano_ind”。错误。我也不能使用它与apply在一个证明。
但是，它应该存在，因为使用Locate Library BinInt.，我可以看到Coq可以找到文件BinInt.vo，而当我打开BinInt.v文件时，我可以看到Lemma peano_ind。
我在Debian9.0+ CoqIDE 8.5pl2和Windows10+ CoqIDE 8.
浏览 9提问于2017-05-19得票数 5
回答已采纳
我成功地安装了coq 8.9.1和coq-Quickchick1.1.0和Opam2.0.4，我正在emacs 26.1上编程。
但是，在运行QuickChick命令时，我收到以下错误：
错误:无法编译mli文件
知道我能做些什么吗？
此外，我还尝试在QuickChick命令之前包含以下命令："QuickChickDebug Debug On“。
然而，没有取得任何成功，也没有提供任何有教育意义的信息。
浏览 2提问于2019-06-11得票数 2
我正在选修“软件基础”课程。无法运行“提取”章节。在第一行Require Coq.extraction.Extraction.失败，并显示消息Coq: Error: Unable to locate library Coq.extraction.Extraction. 我正在CoqIde中运行它。 coqc -v: Coq证明助手，版本8.6 ( 2017年10月)，使用OCaml 4.05.0编译于2017年10月28日14:23:55 CoqIde版本: 8.6 CoqTop参数：-Q /home/evgenii/mysource/coq/coq-excercise/ LF LF 我遗漏
浏览 37提问于2019-05-18得票数 0
回答已采纳
1回答
我试图检查Coq中两个整数之间的等价性，但我得到了这个错误：“术语"first = second”的类型是"Prop“，它不是一个(co-)归纳类型。”Coq中有没有提供等价性检查的库？下面是我的代码： Definition verify_eq (first : Z) (second : Z) : Z :=
if first = second then 0 else 1.
浏览 25提问于2019-02-18得票数 0
回答已采纳
我在开发Angular库时遇到了一个问题: angular-coq。
我正在尝试提供以下功能：
<div ng-controller="myController">
<form coq-model="team1">
<!-- Inputs will be automatically added to form (wrapped in <p>) -->
</form>
</div>
使用在作用域team1中公开的myController，一个具有2个属性的自定义
浏览 1提问于2014-06-13得票数 1
我试图在vscode中使用coq，但似乎无法工作。
错误：
Could not start coqtop (coqtop)
我有这样的选择：
这令人费解，因为我的终端似乎很清楚coq在哪里：
(meta_learning) brandomiranda~/sketching-learning-coq ❯ coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2
(meta_learning) brandomiranda~/sketching-learning-coq ❯ echo $PATH
/Us
浏览 11提问于2022-03-03得票数 2
回答已采纳
我正在尝试使用库函数length_zero_iff_nil，但我似乎无法为coqtop找到正确的Import语句来找到引用。我看过：，所以我开始尝试：
Require Import List.
然后，据说已实现的length是在Coq.Init.Datatypes中定义的：
Require Import Datatype.
然后我看了看：，这意味着：
Require Import Coq.Lists.List.
这些尝试都没有成功。我当然可以证明这是一个小的引理，但由于我正在学习Coq (每天花几个小时在这个问题上)，我也想学习如何使用现有的库，这是我通常能够做到的。这里可能有我缺少的东西，我
浏览 4提问于2016-05-07得票数 1
回答已采纳
1回答
据我所知，Coq有内置的一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但Coq不是定理证明者，Coq是证明助手，这意味着用户需要在每一步中提供一些提示，Coq应该选择什么规则/策略。存在更多的ore - lest组合启发式策略，但Coq仍然不是证明者。我听说过在证明助手中使用机器学习或其他启发式方法来自动化证明过程的努力(它们被命名为*hammer?)，其中一些趋势发表在http://ai4reason.org/activities.html上。 我的问题是- Coq能否被配置为与一阶逻辑的E-prover或Z3 p
浏览 21提问于2019-05-15得票数 3
回答已采纳
我试图编写一个函数，它接受自然数的列表，并将其中不同元素的数量作为输出返回。例如，如果我有列表1,2,2,4,1，函数DifElem应该输出"3“。我尝试过很多事情，最近得到的是：
Fixpoint DifElem (l : list nat) : nat :=
match l with
| [] => 0
| m::tm =>
let n := listWidth tm in
if (~ In m tm) then S n else n
end.
我的逻辑是这样的:如果m不在列表的尾部，那么在计数器中添加一个。如果是的话，不要添加到计数器中
浏览 0提问于2016-04-21得票数 7
回答已采纳
我已经把证据的基本内容简化为几个陈述，即两个不同的单例集的交集是空的，但无法证明这个看似简单的事实。
我已经翻阅过组件库、Powerset事实集、建设性集等等，但是没有找到任何有用的东西。
Require Import Coq.Sets.Ensembles.
Require Import Coq.Strings.String.
Example x: string := "x".
Example y: string := "y".
Lemma ex:
Intersection string (Singleton string x)
(Singleton s
浏览 0提问于2019-05-26得票数 1
回答已采纳
我正在考虑用Coq编写代码并提取这些代码，以便在一个大型Haskell项目中使用。我想在Coq中构建一个模块，证明属性，然后使用Haskell的模块系统来防止违反这些属性(通过智能构造函数)。
我找不到任何迹象表明可以使用显式导出列表将Coq代码提取到Haskell模块中。似乎我必须手动修改提取的Coq代码，这不是什么大问题，但我想知道我是否正确。有没有人有替代方案？
浏览 3提问于2011-09-17得票数 5
回答已采纳
我正在从软件基金会提供的资源中学习coq。在证明鸽子洞原理的过程中，我试图定义一个函数，从列表中提取子序列，这样里面就没有重复的元素。以下是我的定义：
Fixpoint norepeat_subseq {X : Type} (l : list X) : list X :=
match l with
| [] => []
| n :: t => match (In n t) with
| False => n :: norepeat_subseq t
| _ => norepeat_subseq t
浏览 8提问于2022-11-25得票数 0
1回答
我一直在寻找在Coq中讨论与记录相关的子类型的参考资料，但找不到。 我特别想知道Record _ : _ := { _ :> * }语法是什么意思，以及它是如何运行的。尤其是当一条记录有:>和:判断的混合时，我想所有的正常子类型关系(包括排列)都成立？ 请分享您认为相关的其他参考资料(键入规则、子类型在Coq中的实际用法等) 顺便说一句- Agda中有没有类似的机制，如果有的话，欢迎对这一点进行更多的参考。
浏览 26提问于2020-12-16得票数 1
我想使用标准库Coq.Strings.String中的eqb来比较字符串，
但是遵循代码是行不通的。
Require Import String.
Check eqb "foo" "bar".
(*
The reference eqb was not found in the current environment.
Query commands should not be inserted in scripts
*)
我是不是没有正确地使用它，或者我没有成功地构建环境？
$ sw_vers
ProductName: Mac OS X
ProductVe
浏览 0提问于2020-07-14得票数 0
2回答
我试图在我的Windows10机器上使用C++ system()命令执行一个应用程序(Coq编译器)。这是我的代码：
string dospath = "coqc afile.v >> text.txt"; int errorno = system(dospath.c_str());
如果afile.v中存在语法/类型错误，Coq将返回有意义的错误消息。目前，即使Coq返回一个错误(我在text.txt应用程序的命令提示符窗口中看到了错误消息)，在C++中也没有收到任何信息。我想将(任何)消息(由coqc返回)读入text.txt文件中的字符串或文本。我知道有一些
浏览 0提问于2018-05-15得票数 1
2回答
我希望能够有一个地图从任何类型到任何类型的Coq。到目前为止，我已经从标准库中获得了一些成功的using Coq.FSets.FMapList，但是通过执行以下操作，我只能创建关键是自然数的地图。
Require Import Coq.FSets.FMapList.
Require Import Coq.Structures.OrderedTypeEx.
Module Import NatMap := FMapList.Make(Nat_as_OT).
(* whatever I want to do with my NatMap *)
我知道NatMap := FMapList.Make
浏览 14提问于2017-11-18得票数 2
回答已采纳
1回答
我正在尝试跟踪，但是提供的源文件出现了错误，make失败了
make[1]: Entering directory '/home/myhome/Dropbox/org/coq/cpdt'
COQC src/CpdtTactics.v
File "./src/CpdtTactics.v", line 10, characters 0-32:
Error: Cannot find a physical path bound to logical path Omega.
在CpdtTactics.v中
...
Require Import Eqdep List Ome
浏览 15提问于2022-05-19得票数 1
回答已采纳
我正在试着为下面的引理写一个Coq poof：
Require Export Coq.Structures.OrderedTypeEx.
Require Import FMapAVL.
Module M := FMapAVL.Make(Nat_as_OT).
Fixpoint cc (n: nat) (c: M.t nat):bool :=
match M.find n c with
| None => false
| _ => true
end.
Lemma l: forall (n: nat) (k:nat) (m: M.t nat), cc n m = true -&g
浏览 0提问于2017-09-22得票数 0
我使用的是自动Coq8.5 makefile生成器。此makefile以"Top.“作为所有模块的前缀。现在，假设您通过make运行了许多文件，然后希望在IDE中更改/调试某些文件。然后恼人的事实是，Coq抱怨它找不到编译的其他文件，因为在IDE中，它假定名称没有"Top“前缀。我试着调整makefile来去掉这个前缀。但我总是在make的错误消息中结束。谁能告诉我如何删除make中的"Top“前缀，或者告诉IDE使用"Top”前缀。
浏览 2提问于2017-03-31得票数 4
我正在阅读，并下载了它附带的coq脚本。
我使用coq v8.8.1，通过opam安装。
标题中有两个错误，我不知道该如何调试它们。
第二个错误的完整错误消息是
COQDEP VFILES
*警告:在Auto.v文件中，库LF.Maps是必需的，并且未在加载路径中找到！
我的目标是编译和运行Induction.v文件。在得到这些错误之前，我使用coqide的选项首先“makefile”，然后"make“。
浏览 0提问于2019-04-04得票数 3
我正在尝试安装coq用户控制库(MathClasses)之一。在谷歌上搜索了一下之后，我在Coq网站上找到了一个中心git存储库。
在文件之后，我试图通过以下方法获取源代码：
git clone git+ssh://scm.gforge.inria.fr/git/coq-contribs/coq-contribs.git
但我发现了一个错误：
Cloning into 'coq-contribs'...
ssh: connect to host gforge.inria.fr port 22: Connection refused
fatal: Could not read f
浏览 0提问于2015-05-18得票数 2
回答已采纳
我使用的是辅助验证COQ，我的第一个问题是关于Induction.v文件，为什么我们使用Require Export Basics而不是Require Import basics？此外，当我们创建Export basics.v时，它为什么会工作，即使我将基本元素的名称更改为Mybasics.v
Require Export Basics.是做什么的？它是进口还是出口？
我试着在编译归纳之后执行lists.v，但是它不起作用，它说
无法定位库归纳。
我怎么才能解决呢？
浏览 6提问于2017-10-28得票数 0
扫码
添加站长 进交流群
领取专属 10元无门槛券
手把手带您无忧上云
相关资讯
热门标签
云服务器
ICP备案
对象存储
即时通信 IM
腾讯会议活动推荐
腾讯云开发者
