leanprover-community / mathport

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

refactor: split Mathport.Syntax.Translate.Basic #161

Closed gebner closed 2 years ago

gebner commented 2 years ago

The file is used by everything, so any change requires a lot of recompilation. Just as bad, editing trExpr' requires extreme patience since it's at the very end of this long file.