Matita HomeMatita HomeEvery proof step can be immediately executed.
Table 6.2. proof steps
| proof-step | ::= | LCF-tactical | The tactical is applied to each selected sequent. Each new sequent becomes a selected sequent. |
| | | . | The first selected sequent becomes the only one selected. All the remaining previously selected sequents are proposed to the user one at a time when the next "." is used. | |
| | | ; | Nothing changes. Use this proof step as a separator in concrete syntax. | |
| | | [ | Every selected sequent becomes a sibling sequent that constitute a branch in the proof. Moreover, the first sequent is also selected. | |
| | | | | Stop working on the current branch of the innermost branching proof. The sibling branches become the sibling sequents and the first one is also selected. | |
| | | nat[,nat]…: | The sibling sequents specified by the user become the next selected sequents. | |
| | | *: | Every sibling branch not considered yet in the innermost branching proof becomes a selected sequent. | |
| | | skip | Accept the automatically provided instantiation (not shown to the user) for the currently selected automatically closed sibling sequent. | |
| | | ] | Stop analyzing branches for the innermost branching proof. Every sequent opened during the branching proof and not closed yet becomes a selected sequent. | |
| | | focus nat [nat]… | Selects the sequents specified by the user. The selected sequents must be completely closed (no new sequents left open) before doing an "unfocus that restores the current set of sibling branches. | |
| | | unfocus | Used to match the innermost "focus" tactical when all the sequents selected by it have been closed. Until "unfocus" is performed, it is not possible to progress in the rest of the proof. |
Table 6.3. tactics and LCF tacticals
| LCF-tactical | ::= | tactic | Applies the specified tactic. |
| | | LCF-tactical ; LCF-tactical | Applies the first tactical first and the second tactical to each sequent opened by the first one. | |
| | | LCF-tactical [ [LCF-tactical] [| LCF-tactical]… ] | Applies the first tactical first and each tactical in the list of tacticals to the corresponding sequent opened by the first one. The number of tacticals provided in the list must be equal to the number of sequents opened by the first tactical. | |
| | | do nat LCF-tactical | TODO | |
| | | repeat LCF-tactical | TODO | |
| | | first [ [LCF-tactical] [| LCF-tactical]… ] | TODO | |
| | | try LCF-tactical | TODO | |
| | | solve [ [LCF-tactical] [| LCF-tactical]… ] | TODO | |
| | | (LCF-tactical) | Used for grouping during parsing. |