From 4b8a2629c841a8d3eb842c9478315e31874c6c35 Mon Sep 17 00:00:00 2001 From: Dane Sabo Date: Mon, 24 Feb 2025 11:53:40 -0500 Subject: [PATCH] vault backup: 2025-02-24 11:53:40 --- 3-99 Research/LEAN/Tutorial World.md | 1 + 1 file changed, 1 insertion(+) 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 |