Zulip Chat Archive
Stream: general
Topic: lost in translation
Patrick Massot (Mar 11 2019 at 22:14):
What is https://github.com/leanprover/vscode-lean/commit/7d42d7e25091a4c86811cdf40565c6faec4c1ac0#diff-7c2385f0b8db521fe81e3d20489e5f12L939?! How do we get this cross now?
Patrick Massot (Mar 11 2019 at 22:14):
@Edward Ayers Why did you remove it?
Mario Carneiro (Mar 11 2019 at 22:17):
it's \x now
Patrick Massot (Mar 11 2019 at 22:18):
No, it's not
Patrick Massot (Mar 11 2019 at 22:18):
That's a different cross
Patrick Massot (Mar 11 2019 at 22:18):
That was a key component of my Amsterdam talk!
Mario Carneiro (Mar 11 2019 at 22:19):
it's the prod cross
Mario Carneiro (Mar 11 2019 at 22:19):
which cross are you talking about?
Patrick Massot (Mar 11 2019 at 22:19):
I assigned the cross Ed removed to (a fixed version of) prod.map, without any conflict with prod
Kenny Lau (Mar 11 2019 at 22:20):
\X was ⨯ (U+2A2F), and now \x is × (U+00D7)
Mario Carneiro (Mar 11 2019 at 22:20):
it appears to be gone in the translations file now... it's indistinguishable from \times on my monitor
Mario Carneiro (Mar 11 2019 at 22:20):
why are you using notations like this?
Kenny Lau (Mar 11 2019 at 22:21):
⨯ (U+2A2F) is not found in mathlib
Patrick Massot (Mar 11 2019 at 22:21):
That's the point: it's indistinguishable (as it should be) but Lean distinguishes them (because it can't seem to cope with using the same symbol)
Mario Carneiro (Mar 11 2019 at 22:21):
I would suggest reinstating it as \cross
Mario Carneiro (Mar 11 2019 at 22:22):
this is underhanded lean
Mario Carneiro (Mar 11 2019 at 22:23):
most of ed's update is removing a bunch of random unused unicode from the translations file, particularly the weird one-character ones... this looks like a good candidate for removal
Patrick Massot (Mar 11 2019 at 22:24):
How can I get a reasonable symbol for prod.map then?
Mario Carneiro (Mar 11 2019 at 22:24):
<×>?
Patrick Massot (Mar 11 2019 at 22:25):
reasonable?
Mario Carneiro (Mar 11 2019 at 22:25):
I'm not a fan of this crazy unicode overloading
Mario Carneiro (Mar 11 2019 at 22:25):
it makes it very difficult to read and know what's what
Patrick Massot (Mar 11 2019 at 22:25):
This is only a workaround until we get the Parser.
Edward Ayers (Mar 12 2019 at 14:49):
Hi I think I removed it because I didn't realise that U+2A2F was different to U+00D7, I thought it was a duplicate to \x. My policy with cleaning up the translations file was to only remove things which didn't break users' established experience so this was a mistake.
Patrick Massot (Mar 12 2019 at 14:50):
I vote for getting it back
Edward Ayers (Mar 12 2019 at 14:51):
Quick fix -- add this to your settings file:
"lean.input.customTranslations": { "X" : "\u2A2F" }
Edward Ayers (Mar 12 2019 at 14:57):
In general I agree with Mario that using different unicodes which look similar is a bad idea.
· • . ․ ‧ ⋅ ⬝ ∙ ● ⚫ ⬤ 🌑
Edward Ayers (Mar 12 2019 at 14:57):
⁃ ∎ ╸ ╹ ╺ ╻ ━ ■ ▪ ▬ ▮ ◼ ◾ ⬛ ⯀ 🔲
Edward Ayers (Mar 12 2019 at 14:58):
⋄ ◇ ◊ ♢ ✧ ⬦ ⬨ ⬫
Edward Ayers (Mar 12 2019 at 14:58):
‣ ▶ ▸ ▸ ⯈ 🢒
Patrick Massot (Mar 12 2019 at 15:01):
I'm pretty sure we can put that third line to good use
Patrick Massot (Mar 12 2019 at 15:02):
I notice that nobody complained about that cross during my Amsterdam talk
Last updated: Dec 20 2023 at 11:08 UTC