fix indent

server/GameServer/FileWorker.lean

@@ -161,32 +161,32 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (workerState :
             -- Tactic is in the inventory, allow it.
             pure ()
   | .ident info _rawVal val _preresolved =>
-      -- Try to resolve the name
+    -- Try to resolve the name
-      let ns ←
+    let ns ←
-        try resolveGlobalConst (mkIdent val)
+      try resolveGlobalConst (mkIdent val)
-        -- Catch "unknown constant" error
+      -- Catch "unknown constant" error
-        catch | _ => pure []
+      catch | _ => pure []
-      for n in ns do
+    for n in ns do
-        let some (.thmInfo ..) := (← getEnv).find? n
+      let some (.thmInfo ..) := (← getEnv).find? n
-          -- Not a theorem, no checks needed.
+        -- Not a theorem, no checks needed.
-          | return ()
+        | return ()
-        if some n = levelInfo.statementName then
+      if some n = levelInfo.statementName then
-          -- Forbid the theorem we are proving currently
+        -- Forbid the theorem we are proving currently
-          addMessage info inputCtx (severity := .error)
+        addMessage info inputCtx (severity := .error)
-            s!"Structural recursion: you can't use '{n}' to proof itself!"
+          s!"Structural recursion: you can't use '{n}' to proof itself!"
-        let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
+      let theoremsAndDefs := levelInfo.lemmas ++ levelInfo.definitions
-        match theoremsAndDefs.find? (·.name == n) with
+      match theoremsAndDefs.find? (·.name == n) with
-        | none =>
+      | none =>
-          -- Theorem will never be introduced in this game
+        -- Theorem will never be introduced in this game
+        addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
+      | some thm =>
+        -- Theorem is introduced at some point in the game.
+        if thm.disabled then
+          -- Theorem is disabled in this level.
+          addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
+        else if thm.locked then
+          -- Theorem is still locked.
           addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
-        | some thm =>
-          -- Theorem is introduced at some point in the game.
-          if thm.disabled then
-            -- Theorem is disabled in this level.
-            addMessageByDifficulty info s!"The theorem/definition '{n}' is disabled in this level!"
-          else if thm.locked then
-            -- Theorem is still locked.
-            addMessageByDifficulty info s!"You have not unlocked the theorem/definition '{n}' yet!"
 
 where addMessageByDifficulty (info : SourceInfo) (s : MessageData) :=
   -- See `GameServer.FileWorker.WorkerState.difficulty`. Send nothing/warnings/errors