Pcoq: a beginner's tutorial

When you start pcoq, a large window appears on the screen, which should appear approximately as in the following picture.

The top part of this window, just below the menu bar with File, Display, etc. is the area where your work will be recorded. To start this example session you should go into this window and start typing a command, in plain Coq syntax. For this tutorial, we suggest you type the following.

Require Arith.

Click here to proceed

Yves Bertot
Last modified: Tue Feb 1 11:17:11 MET 2000