feat: generate #align commands for alias

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

40 stars 15 forks source link

feat: generate #align commands for alias #217

Closed rwbarton closed 1 year ago

rwbarton commented 1 year ago

I'm sure this is not correct in all edge cases, but hopefully it will only go wrong in obvious ways. Currently, it's very easy to forget to add #aligns for aliases (and it's also a bit inconvenient to do it manually).

rwbarton commented 1 year ago

Fixes #216.