时间戳

首页 > 解决方案 > 如何使用 `coqc` 命令可靠地编译 Coq 代码？

coq - 如何使用 `coqc` 命令可靠地编译 Coq 代码？

问题描述

我正在学习软件基础课程，由于某种原因，我无法获得coqc编译库的命令。

我做了：

coqc Maps.v

但得到错误：

错误：文件 /Users/pinocchio/coq/software_foundations_vol1/Maps.vo 包含库地图而不是库地图

我也尝试使用 coqIDE 进行编译，但出现以下错误：

错误：编译的库 Maps（在文件 /Users/pinocchio/coq/software_foundations_vol1/Maps.vo 中）对库 Coq.Init.Notations 做出不一致的假设

关于我能做什么的任何想法？

标签： coqcoqide

解决方案

推荐阅读