intros gives alpha with diacritics, literally untypable

Stream: general

[Siyuan Yan]

I noticed when given without explicit variable names, introssometimes produce these variable names made of alpha with a breve diacritic. Is this by design? This is super hard to type. Can't even get it with compose key (unless using a greek keyboard layout). (@Julian Berman how do I type these using lean.nvim?)

ᾰ : ∀ (x : ℝ), f (- x) = - f x
ᾰ_1 : ∀ (x : ℝ), g (- x) = - g x

[Andrew Yang]

This is intended to be untypable.

[Julian Berman]

(See e.g. https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Typing.20.E1.BE.B0 )

[Siyuan Yan]

Thanks, I find it hilarious

[Kevin Buzzard]

It was less funny when it was giving weird errors because of variable name clashes -- this is why it was changed

[Mike Shulman]

Wouldn't be better to make the variable actually impossible to refer to, such as by labeling it _, so that users would be more likely to realize that if they want to refer to it they have to give it a name themselves?

[Kevin Buzzard]

That is basically what is done in lean 4, is my understanding.

[Reid Barton]

We were originally going to use a name starting with an underscore but that caused some other issues because it made Lean think it was an internal variable (github discussion thread)

[Reid Barton]

The Lean 4 behavior is much better of course (the variable has a normal name but displayed with a suffixed $\dagger$, and it can't be referred to)