Matita HomeMatita HomeTable of Contents
Table 8.1. tactics
| tactic | ::= | assume id : sterm |
| | | by induction hypothesis we know term ( id ) | |
| | | case id [( id : term )] … | |
| | | justification done | |
| | | justification let id : term such that term ( id ) | |
| | | [obtain id | conclude term] = term [auto_params | using term | using once term | proof] [done] | |
| | | suppose term ( id ) [ that is equivalent to term ] | |
| | | the thesis becomes term | |
| | | we need to prove term [(id )] [ or equivalently term] | |
| | | we proceed by cases on term to prove term | |
| | | we proceed by induction on term to prove term | |
| | | justification we proved term ( id ) |