Pcoq beginner tutorial, step 3

When you have finished typing the text of your command, you can click on the button Do it that appears in the toolbar in the middle of the pcoq window.

Two operations take place. The first operation is that you command is parsed by the pcoq graphical interface and the command is redisplayed that expresses what has been recognized.

The second operation is that your command is sent to Coq where it is executed. As a result, it is redisplayed on a different background (a darker background). As a result, your window should look approximately as in the following figure.

Click here to proceed


Yves Bertot
Last modified: Tue Feb 1 11:48:34 MET 2000