phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

a few examples of the new feature

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-03-03 16:36:13 +01:00
parent ff0adf12c8
commit e6c481a9a4
2 changed files with 3 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+1 -1
View File
@@ -23,7 +23,7 @@ Zeige, dass $A$ wahr ist."
assumption
HiddenHint (A : Prop) (hA : A) : A =>
"Auch hier kann `assumption` den Beweis von `A` finden."
"Auch hier kann `assumption` den Beweis von `{A}` finden."
Conclusion ""
server/testgame/TestGame/Levels/Sum/L04_SumOdd.lean
+2 -2
View File
@@ -33,7 +33,7 @@ $\\sum_{i = 0}^n (2n + 1) = n ^ 2$."
HiddenHint (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 =>
"
Fange wieder mit `induction n` an.
Fange wieder mit `induction {n}` an.
"
HiddenHint : ∑ i : Fin Nat.zero, ((2 : ℕ) * i + 1) = Nat.zero ^ 2 =>
@@ -49,7 +49,7 @@ Den Induktionsschritt startest du mit `rw [Fin.sum_univ_castSucc]`.
HiddenHint (n : ℕ) (hn : ∑ i : Fin n, (2 * (i : ℕ) + 1) = n ^ 2) :
∑ x : Fin n, (2 * (x : ℕ) + 1) + (2 * n + 1) = Nat.succ n ^ 2 =>
"
Hier kommt die Induktionshypothese ins Spiel.
Hier kommt die Induktionshypothese {hn} ins Spiel.
"
HiddenHint (n : ℕ) : n ^ 2 + (2 * n + 1) = Nat.succ n ^ 2 =>