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]`). "