Zulip Chat Archive

I was going to give this as a review comment on the alias PR std4#184, but it seems like the sort of thing that will have people muttering about "increased coordination between std and mathlib", so let's do it via a poll here instead. In short: the current syntax of alias is

alias my_theorem ← alias1 alias2 ...

and I would like to reverse the order to:

alias alias1 := my_theorem

and remove the facility to declare multiple aliases in one command. This is more consistent with other declaration syntaxes (the fact that the declared symbol is on the right in the alias command always trips me up).

Mario Carneiro (Jul 25 2023 at 06:29):

/poll How should alias take its arguments?
alias original_thm <- alias1 alias2
alias alias1 alias2 -> original_thm
alias alias1 -> original_thm (only one declaration allowed)
alias alias1 := original_thm

Mario Carneiro (Jul 25 2023 at 06:35):

There is also the biconditional form of alias:

alias A_iff_B ↔ B_of_A A_of_B
alias A_iff_B ↔ ..

which I think is less suitable for std as is. I'm not sure what kind of syntax would be best for this, perhaps

alias ⟨B_of_A, A_of_B⟩ := A_iff_B

for the first version and omitting the second version entirely. Generating names like this seems very heuristic and not a good fit for a general purpose programming language. (Obviously these can be left in mathlib if they are useful in their current forms.)

Sebastien Gouezel (Jul 25 2023 at 06:44):

I agree that alias ⟨B_of_A, A_of_B⟩ := A_iff_B looks good for the bidirectional version. Maybe allow alias ⟨B_of_A, -⟩ := A_iff_B if one just wants one direction.

Mario Carneiro (Jul 25 2023 at 06:45):

_ is already used to mean "don't generate this direction"

Mario Carneiro (Jul 25 2023 at 06:45):

and I agree we can keep that syntax, although it conflicts if you were hoping that it would mean "generate with an automatic name"

Sebastien Gouezel (Jul 25 2023 at 06:46):

I am all for disabling the automatic name generation.

François G. Dorais (Jul 25 2023 at 10:26):

I just saw this... right after I got done adding support for protected aliases to std4#184. I'm all in favor of the proposal (as well as dropping automatic name generation). Moreover, since alias will now look like a proper declaration, we can add support for modifiers (protected, private, attributes) without reinventing the wheel!