From 17abd2dcf012a37bf509a6daad9ef35f9dd7c4d4 Mon Sep 17 00:00:00 2001
From: Harry Fan <118628756+realharryhero@users.noreply.github.com>
Date: Mon, 2 Sep 2024 16:56:57 -0400
Subject: [PATCH] Specifying exactly what get_premise_definitions obtains

---
 src/lean_dojo/data_extraction/traced_data.py | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/lean_dojo/data_extraction/traced_data.py b/src/lean_dojo/data_extraction/traced_data.py
index 5e56050..87c3a31 100644
--- a/src/lean_dojo/data_extraction/traced_data.py
+++ b/src/lean_dojo/data_extraction/traced_data.py
@@ -838,7 +838,8 @@ def _callback(node: ModuleImportNode, _) -> None:
 
     def get_premise_definitions(self) -> List[Dict[str, Any]]:
         """Return all theorems and definitions defined in the current file that
-        can be potentially used as premises.
+        can be potentially used as premises, including the premises in the theorem
+        statement and premises in the tactics used to prove the theorem. 
 
         Returns:
             List[Dict[str, Any]]: _description_