coq - 如何通过在当前项目中配置 Makefile 或 _Coqproject 来导入其他项目/目录中的文件
问题描述
我想在对当前项目进行编码时导入我的一个项目的文件。
即在./fileB.v中导入文件../ProjectA/fileA.v。
如何通过配置 Makefile 或 _Coqproject 来做到这一点。
解决方案
您在开头添加以下行_CoqProject：
-R ../ProjectA SomeName
然后你应该能够写
From SomeName Require Import fileA.
推荐阅读
- node.js - `napi_throw_type_error` 结构中的`code` 是什么意思？
- java - 在 Spring Cloud Stream 3.x 中不推荐使用 EnableBinding
- python - 使用 GPU 和 Tensorflow 的问题：“没有可在设备上执行的内核映像”
- batch-file - CMD：从 .txt 文件中提取变量字符串
- typescript - 来自 RxJS Observables 的数据流是通过引用还是值？
- react-native - React Native 中的屏幕刷新问题
- python - 无法在 Jupyter 或 iPython 中使用 RDKit
- r - 跨分组数据的横截面相关性并汇总在乳胶表中
- javascript - 使用画布和 javascript 的进度变量
- flutter - 颤振小部件中的问题未在 vscode 中完全生成