Software Installation

Coq installation

We'll use Coq V8.4pl3, take a look at the Coq download page.

Which IDE to use?

The official IDE to edit Coq source code is "CoqIde", which comes with Coq. It's great and you may try it.

There is another popular IDE (my favorite): Proof General, and it's more popular in the Coq community. You may try it.

The installation of proof general is simple:

There are only a few commands you need to know to use ProofGeneral effectively. They are:

What to do next?

Run Proof General. Visit the file Basics.v. And happy hacking.