From c8f7f2caaa0e5581b1f6db5060840c3e26769f4c Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Wed, 31 Jan 2024 12:26:17 +0100
Subject: [PATCH] Update Definitions.lean

---
 Game/Doc/Definitions.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean
index 4559048..00aca4d 100644
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -6,7 +6,7 @@ import GameServer.Commands
 
 -- * `(0 : ℕ)`, an element called zero.
 -- * `(succ : ℕ → ℕ)`, the successor function , i.e. one is `succ 0` and two is `succ (succ 0)`.
--- * `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` seperately.
+-- * `induction` (or `rcases`), tactics to treat the cases $n = 0$ and `n = m + 1` separately.
 
 -- ## Game Modifications