align tag

Stream: mathlib4

[Kevin Buzzard]

Instead of

theorem Foo : ...
#align foo Foo

can we just do

@[align foo]
theorem Foo : ...

instead? I ask because I just mistyped Foo in #align foo Foo and there was no error. In essentially all cases with #align I mean "the theorem I just ported directly above".

[Mario Carneiro]

I've been thinking about doing this as well. It is less clear what mathport should output in this case though; it is more annoying to remove an attribute that mathport redundantly added so probably it should stick to using #align but for user code I don't see why not to support the attribute as well

[Mario Carneiro]

Unfortunately, it is difficult to catch spelling errors on both the lean 3 and lean 4 sides of the attribute, because there are use cases for referencing things that don't exist. At least, you get a hover / go to def on the lean 4 side if you spell it right so that's one way to confirm that things are working. For lean 3 spell check I've been thinking about adding a mathport_lint executable that checks the final result of porting Mathbin::all to ensure that all #aligns are used

[Kevin Buzzard]

aah that would be a nice way to do it. I've just been changing a bunch of theorem names from e.g. option_equiv_sum_punit_symm_inl to optionEquivSumPUnit_symm_inl and I'm worried I'll make a slip.