New alias syntax is coming to Mathlib!

Stream: mathlib4

[François G. Dorais]

Heads up! The new alias syntax discussed earlier is about to land in Mathlib!

It's already active in Std and it will be rolled into Mathlib soon! There is no need for action on your part, everything currently in Mathlib should be patched all at once. (It's been tested a lot so we don't expect major hiccups.)

However, if you are working on a project that is using the old alias command it will break and you will have to fix it. No worries though, the new syntax is designed to be easier to use and closer to the familiar def and theorem commands.

The basic rules are that:

• alias A ← B should become alias B := A
• alias A ↔ B C should become alias ⟨B,C⟩ := A (blanks are allowed for either direction)

As a bonus, the new syntax supports attributes @[...] as well as modifiers: protected, private, etc. These work in the same way they do for theorem and def. However, some seldom used features of the old alias command have been dropped:

• You can no longer declare multiple aliases with the same target in the same line.
• The iff variant no longer supports automatic name generation.

As usual, feel free to ask if you have questions, concerns or run into issues with this transition.

[Mario Carneiro]

I was actually thinking of making mathlib4 alias commmand into a try this, but it's probably already too late for that

[François G. Dorais]

The patch has been merged. Sorry @Mario Carneiro, I wish I had known of your plan earlier.

[François G. Dorais]

I think we need a better system for Mathlib patches from Std. https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Mathlib.20bump.20patches/near/385623850