search

lean-dojo / LeanDojo

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

fix introduced import bug #58

Closed josojo closed 1 year ago

josojo commented 1 year ago

I am very sorry, but my previous merged PR introduced an import bug. (I tried to fix it with AI and trusted too much into it).

I will think about sensible CI improvements, such that we catch contributions errors better. mypy would have caught it for sure :)

yangky11 commented 1 year ago

Thanks!