From 7748eefa4a6df824e024c6f747ff7d55f908e558 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 2 Mar 2023 10:25:18 +0100
Subject: [PATCH] fix lemma check

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

diff --git a/server/leanserver/GameServer/FileWorker.lean b/server/leanserver/GameServer/FileWorker.lean
index cc8a213..3e3cd1e 100644
--- a/server/leanserver/GameServer/FileWorker.lean
+++ b/server/leanserver/GameServer/FileWorker.lean
@@ -92,7 +92,7 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (levelParams :
         let some (.thmInfo ..) := (← getEnv).find? n
           | return () -- not a theroem -> ignore
         let lemmasAndDefs := levelParams.lemmas ++ levelParams.definitions
-        match lemmasAndDefs.find? (fun l => l.name.toString == n) with
+        match lemmasAndDefs.find? (fun l => l.name == n) with
         | none => addErrorMessage info s!"You have not unlocked the lemma/definition '{n}' yet!"
         | some lem =>
           if lem.locked then