search

lean-dojo / LeanDojo

Tool for data extraction and interacting with Lean programmatically.
https://leandojo.org
MIT License
478 stars 72 forks source link

Will LeanDojo Tolerate Theorems That Cannot Be Compiled? #130

Closed tangzhy closed 5 months ago

tangzhy commented 5 months ago

Hi, I have potentially an infinite number of theorems to trace with LeanDojo. Some of these can be successfully compiled, while others cannot. I am wondering if LeanDojo will tolerate theorems that cannot be compiled through?