greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fix typo in Game

Browse Source
This commit is contained in:
Yu-Ting Hsiung
2025-09-27 11:57:21 +08:00
parent fb9970b590
commit ad57f687c0
11 changed files with 15 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/Implication/L02exact2.lean
View File

@@ -17,7 +17,7 @@ Statement (x y : ℕ) (h : 0 + x = 0 + y + 2) : x = y + 2 := by
Hint (hidden := true) "Do that again!
`rw [zero_add] at {h}` tries to fill in
the arguments to `zero_add` (finding `{x}`) then it replaces all occurences of
the arguments to `zero_add` (finding `{x}`) then it replaces all occurrences of
`0 + {x}` it finds. Therefor, it did not rewrite `0 + {y}`, yet."
rw [zero_add] at h
Hint "Now you could finish with `rw [{h}]` then `rfl`, but `exact {h}`

2
Game/Levels/OldProposition/Level_8.lean
View File

@@ -28,7 +28,7 @@ Statement
repeat rw [Not]
```
to get rid of the two occurences of `¬`. (`Not` is the name of `¬`)
to get rid of the two occurrences of `¬`. (`Not` is the name of `¬`)
I'm sure you can take it from there."
Branch