Zulip Chat Archive

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):

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 (Mar 16 2021 at 12:23):

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

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

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"!

Xin Huajian (Oct 03 2022 at 07:58):

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

Riccardo Brasca (Oct 03 2022 at 07:58):

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

Filippo A. E. Nuccio (Oct 03 2022 at 07:59):

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 (Oct 03 2022 at 08:05):

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 (Oct 03 2022 at 08:09):

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 (Oct 03 2022 at 08:09):

you should replace those names with something else

Xin Huajian (Oct 03 2022 at 08:10):

Mario Carneiro said:

you should replace those names with something else

Get it! Thanks!

Mario Carneiro (Oct 03 2022 at 08:11):

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


Last updated: Dec 20 2023 at 11:08 UTC