如何无需加载库，像OCaml一样打印Coq中的定义？

结论：Coq无法像OCaml那样无需加载库就通过全路径直接打印定义。这是因为两者模块系统的设计逻辑存在本质差异：

• OCaml的编译后模块存储在二进制文件中，系统可直接通过路径查找对应符号；
• Coq的编译库文件（.vo）不会被自动扫描，只有通过Require系列命令加载后，目标模块和定义才会进入当前上下文，才能被识别和引用。

不过有几个实用的替代方案可以简化操作：

• 按需加载单个定义：使用From Coq Require Import Arith.Minus(minus_n_O).，仅加载目标定义而非整个模块，减少不必要的上下文加载。
• 命令行一次性执行：在终端运行coqtop -batch -eval 'From Coq Require Import Arith.Minus. Print minus_n_O.'，无需交互式操作即可完成加载和打印。
• 预加载常用库：配置Coq启动文件（如.coqrc），预先导入常用库，每次启动Coq时这些库已在上下文，可直接引用对应定义。

内容的提问来源于stack exchange，提问作者ZhangLiao