From 8ef6a85c10d9912d2f220323ea426e6175c5581b Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Wed, 24 Jan 2024 16:41:38 +0000 Subject: [PATCH] finish tutorial --- Game/Levels/Tutorial/L07add_succ.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Game/Levels/Tutorial/L07add_succ.lean b/Game/Levels/Tutorial/L07add_succ.lean index db13546..e0281c2 100644 --- a/Game/Levels/Tutorial/L07add_succ.lean +++ b/Game/Levels/Tutorial/L07add_succ.lean @@ -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 "