如何在Coq中导入库？

Question

我想用&&作为中的andb的中缀形式。官方文档告诉我&&定义在Coq.Init.Datatypes模块中。 我尝试这样做： Import Coq.Init.Datatypes.

不过勒柯克给出了错误：

Unknown interpretation for notation "_ && _". 

什么是包括在勒柯克标准库的正确方法是什么？

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.