You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
If the Lean 3 input has the form
then the mathport output now contains one
#align add_foo addFoo
resulting fromadd_foo
, and two#align
statements resulting frommul_foo
, because of itsto_additive
instance.This isn't a big deal, because you can just delete the duplicate
#align
command.The text was updated successfully, but these errors were encountered: