Contents Viewing proofs Editing proofs
When you open in the module editor a module containing a theorem wth a proof, you will see a (-) next to the theorem and next to each step that has a subproof. To avoid repeatedly saying step or theorem, we here take a step to be either a theorem or a step of a theorem's proof. Clicking on the (-) next to a step hides the step's proof and changes the (-) to a (+) . Clicking on the (+) undoes the effect of clicking on the (-) .
Right-clicking on a step provides a menu with a section containing the following commands for hiding and revealing parts of the proof of the step at which the cursor is positioned. These commands can also be executed with the indicated pair of keystrokes. If you just type Ctl+G (the first keystroke) and wait a second, you will see a list of all the commands telling you what keystroke you should type next.
BY
or OBVIOUS
proof) that TLAPS can't verify. This command raises a dialog window that allows
you to decompose the proof of the theorem or step into simpler steps.
The dialog contains a
button that raises this help page, which explains
what you can do with this dialog.
<4>
.
A named step begins with a level number and a name, like <4>7
or <4>xy2
(optionally followed by a period).
Putting the cursor on a proof step and executing the Renumber Proof
command causes all the named top-level steps of its proof to be renamed with
consecutive numbers, like <4>1
, <4>2
, etc.
However, you might want to use some meaningful step names like <2>NextImpliesInv1
that you don't want to be turned into numbers.
A module editor
preference provides options to control what step names don't get turned
into numbers.
There is also a preference that determines whether the module should be saved
after executing the command.