8 lines
580 B
Markdown
8 lines
580 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 |
|