minor fix

LeanCopilot/Tactics.lean

@@ -35,18 +35,22 @@ Generate a list of tactic suggestions.
 -/
 def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) := do
   let state ← getPpTacticState
-  let theoremName := match ((← getDeclName?).get!).toString with
+  let nm ← getGeneratorName
+  let model ← getGenerator nm
+  let suggestions ← generate model state targetPrefix
+  -- A temporary workaround to prevent the tactic from using the current theorem.
+  -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
+  let theoremName := match (← getDeclName?).get! |>.toString with
     | "_example" => ""
     | n => n
   let theoremNameMatcher := String.Matcher.ofString theoremName
   if ← isVerbose then
     logInfo s!"State:\n{state}"
-    logInfo s!"Theorem name:¬{theoremName}"
-  let nm ← getGeneratorName
-  let model ← getGenerator nm
-  let suggestions ← generate model state targetPrefix
+    logInfo s!"Theorem name:\n{theoremName}"
   let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
-    if (¬ (theoremName == "") ∧ (Option.isSome <| theoremNameMatcher.find? t)) ∨ (t == "aesop") then none else some (t, s)
+    let isAesop := t == "aesop"
+    let isSelfReference := ¬ (theoremName == "") ∧ (theoremNameMatcher.find? t |>.isSome)
+    if isSelfReference ∨ isAesop then none else some (t, s)
   return filteredSuggestions