如何在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.