leanprover-community / mathport

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

request: produce both #align statements for declarations with @[to_additive] #205

Closed kim-em closed 1 year ago

kim-em commented 2 years ago

We often have to remind people to add #align statements for the additivized statements, and it would be easier if mathport can just do this itself.

rwbarton commented 1 year ago

Fixed by #209.