Skip to content

Commit

Permalink
Merge pull request #205 from realharryhero/main
Browse files Browse the repository at this point in the history
(minor edit) Specifying get_premise_definitions premise locations
  • Loading branch information
yangky11 authored Sep 3, 2024
2 parents 9b19df9 + 17abd2d commit 8b7792a
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/lean_dojo/data_extraction/traced_data.py
Original file line number Diff line number Diff line change
Expand Up @@ -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_
Expand Down

0 comments on commit 8b7792a

Please sign in to comment.