From 6987b4cb01e99471d26a3ff80ae44d2b7e9a1d3d Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 6 Mar 2023 11:29:44 +0100 Subject: [PATCH] levels --- server/testgame/TestGame/LemmaDocs.lean | 3 +++ server/testgame/TestGame/Levels/Function/L02_Let.lean | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean index 46372a3..8bf38bf 100644 --- a/server/testgame/TestGame/LemmaDocs.lean +++ b/server/testgame/TestGame/LemmaDocs.lean @@ -129,3 +129,6 @@ LemmaDoc add_pow_two as add_pow_two in "Nat" LemmaDoc Finset.sum_comm as Finset.sum_comm in "Sum" "" + +LemmaDoc Function.comp_apply as Function.comp_apply in "Function" +"" diff --git a/server/testgame/TestGame/Levels/Function/L02_Let.lean b/server/testgame/TestGame/Levels/Function/L02_Let.lean index d6ea306..247c040 100644 --- a/server/testgame/TestGame/Levels/Function/L02_Let.lean +++ b/server/testgame/TestGame/Levels/Function/L02_Let.lean @@ -66,7 +66,7 @@ HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 => Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 => " -Definitionen muss man anundzu manuell einsetzen um den Taktiken zu helfen. +Definitionen muss man manchmal manuell einsetzen um den Taktiken zu helfen. Das macht man mit `unfold f` (oder alternativ mit `rw [f]`). "