Zulip Chat Archive

Stream: general

Topic: Unicode characters in VS Code


Paul Chisholm (Sep 19 2021 at 23:28):

The ability to use Unicode characters in Lean is a great feature, but entering them as sequences of ASCII characters gets rather tedious. Is there any way to bind those characters to function keys or numpad keys, so for example pressing F1 is equivalent to entering the sequence \ a l l tab.

Kevin Buzzard (Sep 19 2021 at 23:48):

I suspect this is a VS Code question rather than a lean question

Mario Carneiro (Sep 19 2021 at 23:51):

You can always set something like that up in your IME

Mario Carneiro (Sep 19 2021 at 23:52):

It's pretty hard coming up with control sequences that aren't more trouble than those backslash sequences though, since VSCode already has most of them occupied by useful things

Mario Carneiro (Sep 19 2021 at 23:52):

If it is particular sequences that bother you, I think it is possible to make them shorter so that \a means \all or something

Mario Carneiro (Sep 19 2021 at 23:53):

at least, \al and \ex already work if you are after the quantifiers

Paul Chisholm (Sep 20 2021 at 00:59):

Thanks for the info. Not particular sequences, I just want to hit one key for one symbol, particularly in symbol dense code.

I'll chase up the suggestion and ask a question in a VS Code group.

Yaël Dillies (Sep 20 2021 at 11:01):

Buy a mathematical keyboard :upside_down:

Eric Rodriguez (Sep 20 2021 at 11:47):

I'm a strong fan of XCompose/WinCompose - I set caps lock to be my composekey, and then I get stuff like <caps> <A> <A> = alpha (not at my computer rn :[). It's also nice because it's system-wide instead of just on vscode, so can send things in zulip

Johan Commelin (Sep 20 2021 at 11:48):

I got https://github.com/gebner/m17n-lean working this weekend, which is even better than XCompose, I think.

Kevin Buzzard (Sep 20 2021 at 12:46):

but you're still typing \nat to get there, right? My impression is that Paul would rather just be typing N and getting :-)

Johan Commelin (Sep 20 2021 at 12:49):

That's true. But when I type N, I would rather get N.

Johan Commelin (Sep 20 2021 at 12:49):

I can type \N to get

Paul Chisholm (Sep 20 2021 at 21:25):

Actually, what I really want to do is use the function keys or numpad keys so I can hit F1 to get universal quantifier, F2 to get existential quantifier, etc.

Johan Commelin (Sep 21 2021 at 04:04):

How many unicode characters do you intend to type? Here are the ones that I can think of right now that I use very often in mathlib:
∀, ∃, ℕ, ℤ, ℚ, ℝ, ℂ, ⁻¹, ₁, ₂, →, ₐ, ₗ, α, ε, ≤, •, ⊗, ∑, ∏
I probably forgot several other common ones. But certainly, for me, 12 keys wouldn't suffice.

Johan Commelin (Sep 21 2021 at 04:05):

Note that if you don't like typing \N for because of the \, then this is something that you can change. For example, Patrick uses ,, if I'm not mistaken.

Mario Carneiro (Sep 21 2021 at 04:18):

you forgot λ, ←, ⟨, ⟩, ∈

Mario Carneiro (Sep 21 2021 at 04:19):

Actually it might be fun to rank unicode characters by mathlib popularity

Scott Morrison (Sep 21 2021 at 04:30):

αλ→⟨⟩₂₁β←≤∈∀ℕμιℝ∥↔𝕜₀⁻≠⟶¹∃≫γ•∧×≃Πεσ𝓝ℤ₃⊆φ↑ₗ∞≥∘π⥤∑▸∩⊤δ∫∂¬⊓⊥Γ𝟙⊔∣⊗ᶠ∏ℂ∨ν∪⋙≅ℚ⋃∅ᶜₘₐᵥωᵐ⨆⟪⟫∉⊢⦃⦄⨅⁅⁆⊕⇑ᵖτᵒ⟦⟧ϕΣᵢ‹›ₙ₄ₜΦ⋂ψℒ𝕂⬝ö↪η𝓤𝓟𝔸≈ₛ⟮⟯ΨéΛ₊≡↦⟹≪ζᵃ≌√𝓘⁰ℍκ⨁⌊⌋𝟭𝕎θᵀ─χρξᗮë⨯ᵇ⊣↥Δ𝒥ℬ⅟∙◃⊞≺ₖ⇒ₕ₅⌈⌉│⊂∠≼ℱ⨿ℓ○ᵤⁱ⊚⨂ⁿ”“₋ϖ⋊ᘁ⁺𝒄↓₆ₚᴴΩ𝒞–«»‖₇ℰä⊇₈𝒟𝒯𝓢Čò𝓡ⱼ⊙†↾Ιυ§²𝒰∐⋯↿ô ᾰ↟©◫𝒅𝒫∼𝑳ℵₒ…𝑹𝒮ăᵣ𝔭ɱ𝓚·𝒢ᵏ↻𝒪𝔮𝔽à′♯−↗∶⁴↠⌟┌├🎉çêőüℋ’⋁∋³‌⊹📋áí™⇐↘⊑½ᵈ⅓⇉∤✅❌èïł🛑µ‘💥⋆≰≻

Johan Commelin (Sep 21 2021 at 05:39):

Why does ℤ₃ show up on place 35? I mean, I really love the 3-adic numbers, but I didn't expect them that high on the list :rofl:

Kevin Buzzard (Sep 21 2021 at 06:00):

What I don't understand is why on my mobile almost none of the characters in Johan's post display correctly, but almost all of those in Scott's do. Some characters do seem to show up correctly "sometimes" and I've not got to the bottom of what the criterion is

Johan Commelin (Sep 21 2021 at 06:00):

Do these show up correctly?
αλ→⟨⟩₂₁β←≤∈∀ℕμιℝ∥↔𝕜₀⁻≠⟶¹∃≫γ•∧×≃Πεσ𝓝ℤ₃⊆φ↑ₗ∞≥∘π⥤∑▸∩⊤δ∫∂¬⊓⊥Γ𝟙⊔∣⊗ᶠ∏ℂ∨ν∪⋙≅ℚ⋃∅ᶜₘₐᵥωᵐ⨆⟪⟫∉⊢⦃⦄⨅⁅⁆⊕⇑ᵖτᵒ⟦⟧ϕΣᵢ

Johan Commelin (Sep 21 2021 at 06:01):

I just copied the first line of Scott's post into a code block.

Johan Commelin (Sep 21 2021 at 06:01):

How about these:
∀, ∃, ℕ, ℤ, ℚ, ℝ, ℂ, ⁻¹, ₁, ₂, →, ₐ, ₗ, α, ε, ≤, •, ⊗, ∑, ∏

Kevin Buzzard (Sep 21 2021 at 06:01):

How many alphas do I need to turn into G's, R's and M's before lambda regains its rightful place at the top spot?

Kevin Buzzard (Sep 21 2021 at 06:04):

Screenshot_20210921-070304.png

Kevin Buzzard (Sep 21 2021 at 06:04):

You can see from the screenshot that it's perhaps not as easy as "missing font" -- I don't think random events tend to almost always succeed and then suddenly almost always fall

Johan Commelin (Sep 21 2021 at 06:05):

But the problem does have to do with code blocks.

Johan Commelin (Sep 21 2021 at 06:06):

Because all the characters in the "How about these" post are the ones that I first posted in a code block.

Kevin Buzzard (Sep 21 2021 at 06:07):

Screenshot_20210921-070644.png

Sebastian Ullrich (Sep 21 2021 at 07:57):

I was kind of curious about some of these, so here's a quick script outputting counts and a random example per character: https://gist.github.com/Kha/77b9165be43558c574f05f270023381e

Reid Barton (Sep 21 2021 at 11:00):

Scott Morrison said:

αλ→⟨⟩₂₁

This reminds me of how "Second Street" is the most common street name in the US


Last updated: Dec 20 2023 at 11:08 UTC