Merge pull request #15 from hhu-adam/docstrings

better? docstrings
leanprover-community · Aug 6, 2023 · 0e360a1 · 0e360a1
2 parents 134d5cc + f3792e5
commit 0e360a1
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/Game/MyNat/Addition.lean b/Game/MyNat/Addition.lean
@@ -12,11 +12,12 @@ instance : Add MyNat where
   add := MyNat.add
 
 /--
-This theorem proves that if you add zero to a MyNat you get back the same number.
+If `a` is a natural number, then `add_zero a` is the proof that `a + 0 = a`.
 -/
 theorem add_zero (a : MyNat) : a + 0 = a := by rfl
 
 /--
-This theorem proves that (a + (d + 1)) = ((a + d) + 1) for a,d in MyNat.
+If `a` and `d` are natural numbers, then `add_succ a d` is the proof that
+`a + succ d = succ (a + d)`.
 -/
 theorem add_succ (a d : MyNat) : a + (succ d) = succ (a + d) := by rfl
diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean
@@ -1,4 +1,4 @@
-/-- Our copy of the natural numbers called `MyNat`. -/
+/-- Our copy of the natural numbers called `MyNat`, with notation `ℕ`. -/
 inductive MyNat where
 | zero : MyNat
 | succ : MyNat → MyNat