leanprover-community / mathport

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

fix: simplify field name heuristic #227

Closed rwbarton closed 1 year ago

rwbarton commented 1 year ago

When mathport has to translate a field name (f in x.f), the correct result must be already in the FieldNameMap, so the old heuristic did not make a lot of sense. Now we at least use a name that exists. This is more of an issue since the introduction of "smart naming" which sometimes generates names_likeThis.