Zulip Chat Archive

Stream: new members

Topic: Typing ᾰ


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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_ᾰ).

view this post on Zulip Johan Commelin (Mar 16 2021 at 12:17):

What are you taking cases of?

view this post on Zulip Johan Commelin (Mar 16 2021 at 12:17):

Does it need more than one name?

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 16 2021 at 12:23):

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

view this post on Zulip Guilherme Espada (Mar 16 2021 at 12:30):

Thanks!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kenny Lau (Mar 16 2021 at 14:48):

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

view this post on Zulip 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...

view this post on Zulip 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 )

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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