Skip to content

Commit

Permalink
remove get_namespaces
Browse files Browse the repository at this point in the history
  • Loading branch information
Kaiyu Yang committed Apr 26, 2024
1 parent d2b5903 commit f8f4c8e
Showing 1 changed file with 0 additions and 7 deletions.
7 changes: 0 additions & 7 deletions src/lean_dojo/data_extraction/traced_data.py
Original file line number Diff line number Diff line change
Expand Up @@ -344,13 +344,6 @@ def get_single_tactic_proof(self) -> Optional[str]:

return proof

def get_namespaces(self) -> Tuple[List[str], List[str]]:
"""Return the namespaces that the theorem is located in,
as well as the namespaces that are merely open.
"""
assert self.traced_file is not None
return self.traced_file.get_namespaces(self)

def get_premise_full_names(self) -> List[str]:
"""Return the fully qualified names of all premises used in the proof."""
names = []
Expand Down

0 comments on commit f8f4c8e

Please sign in to comment.