coq - 有没有办法取消导入或隐藏基本库？

Question

有没有办法在 coq 中取消导入或隐藏基础库？

Answer 1

-nois您可以通过传递给coqtop或来避免包含标准库coqc。

也可以创建不同的初始状态（您可以将其传递给-is.这有一些代码可以做到这一点（同时没有其他有趣的东西）。