search

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4
Apache License 2.0
43 stars 15 forks source link

feat: skip defeq check for synport #187

Closed digama0 closed 2 years ago

digama0 commented 2 years ago

This solves the issue of ₓ in all the definitions, as well as significantly improving the performance of synport. You probably want to keep the skipDefEq option off if you are using the Mathbin compiled olean files, but for synport it's just a waste of cycles to check defeqs when we are often explicitly interested in breaking these defeqs in practice.

Fixes #170

gebner commented 2 years ago

You probably want to keep the skipDefEq option off if you are using the Mathbin compiled olean files

Everyone uses the default releases though, so if we enable skipDefEq then they'll have to take it.

Personally, I think we can drop import Mathbin support if this helps with the port. But I just want us to be clear that we are dropping it.