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

hint for add_succ

Browse Source
This commit is contained in:
Kevin Buzzard
2023-12-22 14:56:28 +00:00
parent 9e90d25642
commit cfe1ae17d5
1 changed files with 2 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
Game/Levels/Tutorial/L07add_succ.lean
View File

@@ -40,7 +40,8 @@ see which proofs you can rewrite.
/-- For all natural numbers $a$, we have $\operatorname{succ}(a) = a+1$. -/ /-- For all natural numbers $a$, we have $\operatorname{succ}(a) = a+1$. -/
Statement succ_eq_add_one n : succ n = n + 1 := by Statement succ_eq_add_one n : succ n = n + 1 := by
Hint (hidden := true) "First unravel the `1`." Hint "Start by unravelling the `1`."
Hint (hidden := true) "`rw [one_eq_succ_zero]` will do this."
rw [one_eq_succ_zero] rw [one_eq_succ_zero]
Hint (hidden := true) "Now you can `rw [add_succ]`" Hint (hidden := true) "Now you can `rw [add_succ]`"
rw [add_succ] rw [add_succ]