From 87cbcbc4e00787c14ccfda96ca23f304d4b48992 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <3138005+Smaug123@users.noreply.github.com>
Date: Sat, 25 Nov 2023 22:49:16 +0000
Subject: [PATCH] Grammar fix in FileWorker.lean

---
 server/GameServer/FileWorker.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean
index 0cca9c1..9d1dd30 100644
--- a/server/GameServer/FileWorker.lean
+++ b/server/GameServer/FileWorker.lean
@@ -109,7 +109,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext)
           | return () -- not a theorem -> ignore
         -- Forbid the theorem we are proving currently
         if n = levelParams.statementName then
-          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to proof itself!"
+          addErrorMessage info inputCtx s!"Structural recursion: you can't use '{n}' to prove itself!"
 
         let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
         match lemmasAndDefs.find? (fun l => l.name == n) with