search

openai / lean-gym

Apache License 2.0
150 stars 31 forks source link

Accessing the Global Environment #25

Closed yangky11 closed 1 year ago

yangky11 commented 1 year ago

Hi,

Thanks for providing a great tool! I wonder whether it is possible to access the global environment (e.g., existing definitions and theorems either in the same file or imported from other files) using lean-gym. Thanks!