lean-dojo / LeanDojo

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

Do not list the theorem itself as premise #92

Closed josojo closed 9 months ago

josojo commented 9 months ago

WIth the lastest modifications, we are listing the theorem itself as a premise to the theorem itself.

This is because the ExtractData script visits a def/theorem itself within visitTermInfo while parsing.

yangky11 commented 9 months ago

thx