Typing ᾰ

Stream: new members

[Guilherme Espada]

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]

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

[Johan Commelin]

@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]

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]

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]

What are you taking cases of?

[Johan Commelin]

Does it need more than one name?

[Guilherme Espada]

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]

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

[Johan Commelin]

Guilherme Espada said:

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]

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

[Guilherme Espada]

Thanks!

[Eric Wieser]

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]

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

[Kenny Lau]

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

[Damiano Testa]

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]

(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]

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]

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]

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]

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

[Xin Huajian]

How to typing ᾰ? It seems doesn't occur in https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

[Riccardo Brasca]

Why do you want to type it? The character has been chosen exactly because it's nearly impossibly to type...

[Filippo A. E. Nuccio]

Well, and there is a reason for this: the character is inserted automatically and it is supposed to never clash with users' variables. That's why it was chosen: it is hard to type...

[Damiano Testa]

If you find that you want to refer to it, you likely have a way of assigning yourself a name to the hypothesis and then you can use it. Did it appear as a consequence of intros or some other tactic to which you could have given explicit identifiers?

If you cannot give it a name, then there may be some weird unreachable stuff going on.

[Xin Huajian]

Cause the "Generate a list of equations for a recursive definition" by typing {! ... !} in VS Code would generate equations using ᾰ, like
| (var ᾰ) := _ | (sort ᾰ) := _
then if I want to follow this suggestion, maybe I should use ᾰ?

[Mario Carneiro]

you should replace those names with something else

[Xin Huajian]

Mario Carneiro said:

you should replace those names with something else

Get it! Thanks!

[Mario Carneiro]

the autogenerated equations use the default names, which sometimes comes from binders in the original source so they aren't completely useless, but if the original binders were from an anonymous forall from A -> B then there is no better name to invent