Merge pull request #43 from lean-dojo/dev

Ignore namespace prefix to theorem names
lean-dojo · Dec 10, 2023 · 6c0976c · 6c0976c
2 parents f84d2a6 + c804ed8
commit 6c0976c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/LeanCopilot/LlmAesop.lean b/LeanCopilot/LlmAesop.lean
@@ -19,7 +19,7 @@ def tacGen : Aesop.TacGen := fun (mvarId : MVarId) => do
   -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
   let theoremName := match (← liftM (m := MetaM) <| Term.TermElabM.run getDeclName?).1.get! |>.toString with
     | "_example" => ""
-    | n => n
+    | n => (n.splitOn ".").getLast!
   let theoremNameMatcher := String.Matcher.ofString theoremName
   let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
     let isAesop := t == "aesop"

diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
@@ -42,7 +42,7 @@ def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) :
   -- TODO: Use a more pincipled way, e.g., see Lean4Repl.lean in LeanDojo.
   let theoremName := match (← getDeclName?).get! |>.toString with
     | "_example" => ""
-    | n => n
+    | n => (n.splitOn ".").getLast!
   let theoremNameMatcher := String.Matcher.ofString theoremName
   if ← isVerbose then
     logInfo s!"State:\n{state}"