coq - 如何在 Coq 中导入库？

Question

我想在 Coq 中使用 && 作为 andb 的中缀形式。官方文档告诉我 && 是在 Coq.Init.Datatypes 模块中定义的。我试过这个:导入 Coq.Init.Datatypes。

Coq 仍然给出错误:

Unknown interpretation for notation "_ && _".

在 Coq 中包含 Std 库的正确方法是什么？

Answer 1

您可以使用Locate命令获取有关此的一些信息:

Locate "&&".

这是它的输出:

Notation            Scope
"x && y" := andb x y : bool_scope

manual说的是

The initial state of Coq declares three interpretation scopes and no lonely notations. These scopes, in opening order, are core_scope, type_scope and nat_scope.

如您所见，&& 表示法所在的 bool_scope 默认情况下未打开。

您可以明确指定范围:

Check (true && false) % bool.

或者像这样打开它:

Open Scope bool_scope.
Check true && false.