## Stream: new members

### Topic: Typing ᾰ

#### Guilherme Espada (Mar 16 2021 at 12:04):

After upgrading lean, ᾰ often appears in local context names. How do I type this character?

In addition, is there a list of char shortcuts anywhere?

#### Ruben Van de Velde (Mar 16 2021 at 12:06):

The idea is that you don't type it, but pick your own names instead

#### Johan Commelin (Mar 16 2021 at 12:10):

@Guilherme Espada here's the reason: tactics need to choose names for hypotheses that they introduce. Usually, they except as arguments a list of names that they will use. For example intros x y z.
Now, more or less, the default name that tactics used was a. And if users already had some a in context, it would now be shadowed, which led to the a-bug, which was very annoying.
So it was decided to replace the default name by something ugly that is very hard to type.

#### Johan Commelin (Mar 16 2021 at 12:11):

In general, using auto-generated names can be nice for small proofs, but they are a hazard for maintaining a large library like mathlib.

#### Guilherme Espada (Mar 16 2021 at 12:16):

Ah, I suspected so because the choice seemed weird to me.
I guess my question then is: how do you rename the results of cases? cases p with p_a(which is mentioned in the docs) doesn't seem to rename the variable, at least not in my example (the name is still p_ᾰ).

#### Johan Commelin (Mar 16 2021 at 12:17):

What are you taking cases of?

#### Johan Commelin (Mar 16 2021 at 12:17):

Does it need more than one name?

#### Guilherme Espada (Mar 16 2021 at 12:20):

Well, yes, there are are quite a few options. But only one is viable (the rest are automatically eliminated). Do I need to list out names for each of the options?

#### Scott Morrison (Mar 16 2021 at 12:22):

(You might also try using rcases, which has better syntax when naming the sub-pieces of complicated things.)

#### Johan Commelin (Mar 16 2021 at 12:23):

Well, yes, there are are quite a few options. But only one is viable (the rest are automatically eliminated). Do I need to list out names for each of the options?

Well, it will use the first name you provide for the first option

#### Johan Commelin (Mar 16 2021 at 12:23):

So you might need to write cases p with _ _ _ _ p_a _ _

Thanks!

#### Eric Wieser (Mar 16 2021 at 13:03):

Should we add a vscodeshortcut /dont_type_this_use_explicit_names_instead so that when you hover over ᾰ in vs-code it shows you that?

#### Eric Wieser (Mar 16 2021 at 13:09):

Or to be super mean, /ᾰ_should_not_be_typed, so that there's no chance of anyone using it

#### Kenny Lau (Mar 16 2021 at 14:48):

On the Greek polytonic keyboard on Windows, ᾰ can be typed by typing Shift + - and then a.

#### Damiano Testa (Mar 16 2021 at 14:49):

I had never thought about this, but there is no such thing as a short ω or η in the (ancient) Greek language: that could have been an even harder-to-achieve symbol...

#### Julian Berman (Mar 16 2021 at 14:49):

(Also, in case it's useful for other ones, the list of abbreviations is here: https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json )

#### Guilherme Espada (Mar 16 2021 at 14:57):

I feel bad for using the symbol (against the advice of the lovely people of this chat), but it's a one-off project that won't be published, so I feel less bad

#### Yakov Pechersky (Mar 16 2021 at 15:08):

Instead of using the symbol, you can use french quotes:

example (h : 0 < 0) : true :=
begin
exact absurd (le_refl _) ‹0 < 0›.not_le
end


#### Kenny Lau (Mar 16 2021 at 15:43):

Damiano Testa said:

I had never thought about this, but there is no such thing as a short ω or η in the (ancient) Greek language: that could have been an even harder-to-achieve symbol...

right, but you also don't have epsilon/eta/omicron/omega with vrachy

#### Damiano Testa (Mar 16 2021 at 15:47):

:lol: There are so many diacritic symbols that "look the same"!

Last updated: May 10 2021 at 17:39 UTC