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

Typo: remove extra word to

Browse Source
This commit is contained in:
dharmatech
2025-09-26 22:17:35 -07:00
committed by GitHub
parent fb9970b590
commit e6e15d8b07
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
Game/Levels/Addition/L01zero_add.lean
View File

@@ -55,7 +55,7 @@ Statement zero_add (n : ℕ) : 0 + n = n := by
Hint (hidden := true) "try rewriting `add_zero`." Hint (hidden := true) "try rewriting `add_zero`."
rw [add_zero] rw [add_zero]
rfl rfl
· Hint "Now for to the second goal. Here you have the induction hypothesis · Hint "Now for the second goal. Here you have the induction hypothesis
`{hd} : 0 + {d} = {d}`, and you need to prove that `0 + succ {d} = succ {d}`." `{hd} : 0 + {d} = {d}`, and you need to prove that `0 + succ {d} = succ {d}`."
Hint (hidden := true) "Use `add_succ`." Hint (hidden := true) "Use `add_succ`."
rw [add_succ] rw [add_succ]