Matita HomeMatita HomeTable of Contents
Table 7.1. tactics
| tactic | ::= | @ sterm |
| | | applyS sterm auto_params | |
| | | assumption | |
| | | /auto_params/. | |
| | | cases term pattern | |
| | | change pattern with sterm | |
| | | -id | |
| | | % [nat] [{sterm…}] | |
| | | cut sterm | |
| | | * [as id] | |
| | | destruct [(id…)] [skip (id…)] | |
| | | elim sterm pattern | |
| | | generalize pattern | |
| | | # id | |
| | | #_ | |
| | | inversion sterm | |
| | | lapply sterm | |
| | | letin id ≝ sterm | |
| | | ## | |
| | | normalize pattern [nodelta] | |
| | | [<|>] sterm pattern | |
| | | whd pattern [nodelta] |