There are 3 view parts in the interface:
the editor, which is used to view a Coq file. It has syntax highlighting,
and when a part is evaluated, the part cannot be edited anymore (as in most
interactive theorem prover editors).
- the top-level, use to show the result of the interactions.
- the outline not shown for every prover, which able to view a summary
of the currently edited files.
3.1.2 Evaluating a file
All the interactions are done through the usse of a toolbar.
From left to right, the meanings of the buttons:
Some of these commands are binded to some keyboard shortcuts as detailed
in the next section.
the first one launch or reset Prover Editor on the currently read file.
- the second is used to progress through a proof
- the third is made to undo a step in a proof
- the fourth is made to try to progress until the end of the
currently edited file
- the fifth is bound to go back to the beginning of a file
- the sixth one, is to cancel the current interaction with the
prover. This last button is to use with the first button, as it is useful
to restart everything if we are in an inconsistent state of the editor
(it should not happen really often, but it is useful to be able to
reset the editor state).