How to import libraries in Coq?

Question

I want to use && as infix form of andb in Coq. Official documentation tells me && is defined in Coq.Init.Datatypes module. I tried this:

Import Coq.Init.Datatypes.

Still Coq gives error:

The command has indeed failed with message:
Unknown interpretation for notation "_ && _".

What is the correct way to include Std library in Coq?

Answer

You can use the Locate command to get some information on this:

Locate "&&".
Notation "x && y" := (andb x y) : bool_scope

Here is its output:

Notation "x && y" := (andb x y) : bool_scope

The manual says that

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.

As you can see, bool_scope where the && notation lives isn't open by default.

You can either specify the scope explicitly:

Check (true && false) % bool.
(true && false)%bool
     : bool

or open it like so:

Open Scope bool_scope.
Check true && false.
true && false
     : bool