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