不加载库打印Coq定义

Question

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.Minus.minus_n_O. 

有没有一种不像在Print Coq.Arith.Minus.minus_n_O中应用函数那样不加载库就可以运行OCaml的方法？

Answer 1

在Coq中，需要模块和导入模块是有区别的。Require是一个关键字，它允许您加载库，而Import允许您删除前缀。Export M做Import M，但也说当当前模块本身被导入时，M也会被导入。

我会说你想要的是

From Coq Require Arith.Minus.
Print Coq.Arith.Minus.minus_n_O. 

没有Export。

与ocaml相比，Import类似于open，而Require只是隐含在ocaml中:模块在基本使用时被导入。

您可以在进口文件、导出和要求中找到更多信息。另外，要想找到更多关于命令的信息，只需查找命令索引即可。