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

finish tutorial

Browse Source
This commit is contained in:
Kevin Buzzard
2024-01-24 16:41:38 +00:00
parent 9f00207bb7
commit 8ef6a85c10
1 changed files with 1 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -15,8 +15,8 @@ TheoremDoc MyNat.add_succ as "add_succ" in "+"
NewTheorem MyNat.add_succ
/-- `succ_eq_add_one n` is the proof that `succ n = n + 1`. -/
TheoremDoc MyNat.succ_eq_add_one as "succ_eq_add_one" in "+"
"`succ_eq_add_one n` is the proof that `succ n = n + 1`."
Introduction
"