个人中心
文章发布
退出
作者热门文章
- html - 出于某种原因，IE8 对我的 Sass 文件中继承的 html5 CSS 不友好？
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景？
24
4
我使用 OPAM 安装 bignum
$ opam upgrade bignum
Already up-to-date.
Require Import BigN.导入了库但是
coqc bignum_problem产生响应
File "./bignum_problem.v", line 1, characters 15-19:
Error: Unable to locate library
BigN.
最佳答案
看来bignum指的是 OCaml 库；您可能想要安装 coq-bignums反而。我刚刚在我的机器上安装了那个库，并且能够要求 BigN用命令
From Bignums Require Import BigN.
关于coq - 使用 coqide，命令 `Require Import BigN` 在 coq 8.6 中有效，但在 coq 8.7 中无效，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/47007505/
24
4
0
我无法加载 CoqIde 中同一文件夹中的模块。 我正在尝试从 Software Foundations 加载源代码，我在包含带有 coqide 的 SF 源代码的文件夹中运行 coqide或 coq
我正在运行 CoqIDE 来阅读系列教科书“软件基础”，我目前正在阅读“逻辑基础”卷。我刚刚开始第 2 章(归纳)，但是当我尝试运行该行时 From LF Require Import Basics.
我是 Coq 新手，因此为了提高我对证明检查的理解，我尝试使用 Ssreflect 库。 我已经在终端上运行的 Mac OS v 10.10.3 ( Yosemite ) 上安装了 Ssreflect
我已经安装了coq和 CoqIDE通过 opam ，按照说明 here . 如说明中所述，每次我必须 export OPAMROOT=~/opam-coq.8.9.0 eval `opam confi
我正在使用自动 Coq 8.5 生成文件生成器。这个 makefile 以“Top”作为所有模块的前缀。 . 现在假设您通过 make 运行了很多文件，然后想要在 IDE 中更改/调试某些文件。 然后
我在 Ubuntu 17.04 中全新安装了 Coq 8.6。当我尝试使用 make 编译我的项目时，它工作正常，直到我收到第一条错误消息。然后，我尝试使用 CoqIDE 来定位并纠正错误，但是我得到
我在 mac os X 上使用 CoqIDE_8.4pl5。当 CoqIDE 转发到此命令时，会弹出此错误消息:需要导入基础知识。 错误:编译的库 Basics.vo 对库做出了不一致的假设Coq.I
我有两个短文件:cc_test 由引理 cc: 4 = 4. 证明。汽车。 Qed.libtest 由需要导入 cc_test。检查抄送。 当我执行coqc -R 。 ClosureLib -top
我使用 OPAM 安装 bignum $ opam upgrade bignum Already up-to-date. 在 coq 8.6 中，代码 Require Import BigN.导入了库
我是一名优秀的程序员,十分优秀！