double #align with toAdditive to existing definition

leanprover-community / mathport

Mathport is a tool for porting Lean3 projects to Lean4

Apache License 2.0

40 stars 15 forks source link

double #align with toAdditive to existing definition #221

Open rwbarton opened 1 year ago

rwbarton commented 1 year ago

If the Lean 3 input has the form

def add_foo := ...
@[to_additive]
def mul_foo := ...

then the mathport output now contains one #align add_foo addFoo resulting from add_foo, and two #align statements resulting from mul_foo, because of its to_additive instance. This isn't a big deal, because you can just delete the duplicate #align command.