Coqでライブラリをインポートするには？

Question

&&をcoqのandbの埋め込みフォームとして使用したいと思います。公式のドキュメントは&&がCoq.Init.Datatypesモジュールで定義されていることを伝えます。 私はこれを試してみました： Import Coq.Init.Datatypes.

それでもコックが与えるエラー：

Unknown interpretation for notation "_ && _". 

コックに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.