diff --git a/3-99 Research/LEAN/Tutorial World.md b/3-99 Research/LEAN/Tutorial World.md index 943fdc7e3..74fc0e930 100644 --- a/3-99 Research/LEAN/Tutorial World.md +++ b/3-99 Research/LEAN/Tutorial World.md @@ -5,3 +5,4 @@ | `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 |