9 lines
675 B
Markdown
9 lines
675 B
Markdown
# Tactics
|
|
| Tactic Name | Ex. Expr. | What does it do? |
|
|
| ----------- | ------------ | ------------------------------------------------------------- |
|
|
| `rfl` | $X = X$ | Proves all theorems of the observed form. |
|
|
| `rw [h]` | $Y = X+a$ | 'Rewrite' an equation using an assumption 'h' or similar. |
|
|
| `succ x` | $Y = Y+1$ | 'Successor' says that some number is bigger than another one. |
|
|
| `\l` | $\leftarrow$ | Does the opposite of rw. Turns Ys into Xs |
|
|
| `repeat` | n/a | Repeats the following action |
|