From 5bb0c9e6fb7ca12b9fa6a451a2fba4c843f752a6 Mon Sep 17 00:00:00 2001 From: Martin Leduc <31558169+DecimalTurn@users.noreply.github.com> Date: Thu, 28 Nov 2024 22:17:32 -0500 Subject: [PATCH 1/2] Fix terminology in L02rw.lean --- Game/Levels/Tutorial/L02rw.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean index 86c21c6..564d1b0 100644 --- a/Game/Levels/Tutorial/L02rw.lean +++ b/Game/Levels/Tutorial/L02rw.lean @@ -164,7 +164,7 @@ your list of assumptions. Lean thinks of `h` as being a secret proof of the assumption, rather like `x` is a secret number. Before we can use `rfl`, we have to \"substitute in for $y$\". -We do this in Lean by *rewriting* the proof `h`, +We do this in Lean by *rewriting* the assumption `h`, using the `rw` tactic. " From e9a2e0a4c3a3987f5dcd675a09cc5c8d6b796d40 Mon Sep 17 00:00:00 2001 From: Martin Leduc <31558169+DecimalTurn@users.noreply.github.com> Date: Sun, 1 Dec 2024 22:43:45 -0500 Subject: [PATCH 2/2] Update Game/Levels/Tutorial/L02rw.lean Co-authored-by: Jon Eugster --- Game/Levels/Tutorial/L02rw.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Tutorial/L02rw.lean b/Game/Levels/Tutorial/L02rw.lean index 564d1b0..fb694dd 100644 --- a/Game/Levels/Tutorial/L02rw.lean +++ b/Game/Levels/Tutorial/L02rw.lean @@ -164,7 +164,7 @@ your list of assumptions. Lean thinks of `h` as being a secret proof of the assumption, rather like `x` is a secret number. Before we can use `rfl`, we have to \"substitute in for $y$\". -We do this in Lean by *rewriting* the assumption `h`, +We do this in Lean by *rewriting* the proof with `h`, using the `rw` tactic. "