Update Definitions.lean

2023-10-26 17:45:48 +02:00
parent 99e1017361
commit 7e7bdc6c06
1 changed files with 1 additions and 1 deletions
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -13,7 +13,7 @@ import GameServer.Commands
 -- This notation is for our own version of the natural numbers, called `MyNat`.
 -- The natural numbers implemented in Lean's core are called `Nat`.

-- If you end up getting someting of type `Nat` in this game, you probably
+-- If you end up getting something of type `Nat` in this game, you probably
 -- need to write `(4 : ℕ)` to force it to be of type `MyNat`.

 -- *Write with `\\N`.*