如何导入Coq库？

Question

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

Coq仍然给出了错误：

Unknown interpretation for notation "_ && _".

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

Answer 1

您可以使用Locate命令获取有关以下内容的信息：

Locate "&&".

这是它的产出：

符号范围"x & y“:=和b x y: bool_scope

手册说

Coq的初始状态声明了三个解释范围，没有单独的符号。按开头顺序，这些范围是core_scope、type_scope和nat_scope。

正如您所看到的，在默认情况下，bool_scope标记所在的&&符号并不是打开的。

您可以显式地指定作用域：

Check (true && false) % bool.

或者像这样打开它：

Open Scope bool_scope.
Check true && false.