Unicode characters in VS Code

Stream: general

[Paul Chisholm]

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]

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

[Mario Carneiro]

You can always set something like that up in your IME

[Mario Carneiro]

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]

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]

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

[Paul Chisholm]

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]

Buy a mathematical keyboard :upside_down:

[Eric Rodriguez]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

I can type \N to get ℕ

[Paul Chisholm]

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]

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]

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]

you forgot λ, ←, ⟨, ⟩, ∈

[Mario Carneiro]

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

[Scott Morrison]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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]

Screenshot_20210921-070304.png

[Kevin Buzzard]

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]

But the problem does have to do with code blocks.

[Johan Commelin]

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

[Kevin Buzzard]

Screenshot_20210921-070644.png

[Sebastian Ullrich]

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]

Scott Morrison said:

αλ→⟨⟩₂₁

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