From 50b6f68a6f486a4ea9ec68e40de69f00475748ad Mon Sep 17 00:00:00 2001
From: Peiyang-Song <p_song@ucsb.edu>
Date: Sat, 9 Dec 2023 00:08:50 -0800
Subject: [PATCH] Detect if theorem name is contained

---
 LeanCopilot/Tactics.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/LeanCopilot/Tactics.lean b/LeanCopilot/Tactics.lean
index 431252d..551dd1e 100644
--- a/LeanCopilot/Tactics.lean
+++ b/LeanCopilot/Tactics.lean
@@ -2,6 +2,7 @@ import Lean
 import LeanCopilot.Options
 import LeanCopilot.Frontend
 import Aesop.Util.Basic
+import Std.Data.String.Basic
 
 open Lean Meta Elab Term Tactic
 
@@ -37,6 +38,7 @@ def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) :
   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}"
@@ -44,7 +46,7 @@ def suggestTactics (targetPrefix : String) : TacticM (Array (String × Float)) :
   let model ← getGenerator nm
   let suggestions ← generate model state targetPrefix
   let filteredSuggestions := suggestions.filterMap fun ((t, s) : String × Float) =>
-    if (t == theoremName) ∨ (t == "aesop") then none else some (t, s)
+    if (¬ (theoremName == "") ∧ (Option.isSome <| theoremNameMatcher.find? t)) ∨ (t == "aesop") then none else some (t, s)
   return filteredSuggestions