Matita HomeMatita HomeTable of Contents
Table 7.1. tactics
| tactic | ::= | absurd sterm |
| | | apply sterm | |
| | | applyS sterm auto_params | |
| | | assumption | |
| | | auto auto_params. autobatch auto_params | |
| | | cases term pattern [([id]…)] | |
| | | change pattern with sterm | |
| | | clear id [id…] | |
| | | clearbody id | |
| | | compose [nat] sterm [with sterm] [intros-spec] | |
| | | constructor nat | |
| | | contradiction | |
| | | cut sterm [as id] | |
| | | decompose [as id…] | |
| | | demodulate auto_params | |
| | | destruct sterm | |
| | | elim sterm pattern [using sterm] intros-spec | |
| | | elimType sterm [using sterm] intros-spec | |
| | | exact sterm | |
| | | exists | |
| | | fail | |
| | | fold reduction-kind sterm pattern | |
| | | fourier | |
| | | fwd id [as id [id]…] | |
| | | generalize pattern [as id] | |
| | | id | |
| | | intro [id] | |
| | | intros intros-spec | |
| | | inversion sterm | |
| | | lapply [linear] [depth=nat] sterm [to sterm [,sterm…] ] [as id] | |
| | | left | |
| | | letin id ≝ sterm | |
| | | normalize pattern | |
| | | reflexivity | |
| | | replace pattern with sterm | |
| | | rewrite [<|>] sterm pattern | |
| | | right | |
| | | ring | |
| | | simplify pattern | |
| | | split | |
| | | subst | |
| | | symmetry | |
| | | transitivity sterm | |
| | | unfold [sterm] pattern | |
| | | whd pattern |