From 0ea112c29e8fdf6b4c9cae2f312d466f97450ef2 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 25 Apr 2023 14:13:18 +0200 Subject: [PATCH] fix --- server/nng/NNG/Levels/Addition/Level_1.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/server/nng/NNG/Levels/Addition/Level_1.lean b/server/nng/NNG/Levels/Addition/Level_1.lean index 884d82a..03b7d95 100644 --- a/server/nng/NNG/Levels/Addition/Level_1.lean +++ b/server/nng/NNG/Levels/Addition/Level_1.lean @@ -34,7 +34,7 @@ note that `zero_add` is about zero add something, and `add_zero` is about someth The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`. " -Statement MyNat.zero_add (attr := simp) +Statement MyNat.zero_add "For all natural numbers $n$, we have $0 + n = n$." (n : ℕ) : 0 + n = n := by Hint "You can start a proof by induction over `n` by typing: