Zulip Chat Archive

Stream: general

Topic: lost in translation


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

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:14):

@Edward Ayers Why did you remove it?

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:17):

it's \x now

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:18):

No, it's not

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:18):

That's a different cross

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:18):

That was a key component of my Amsterdam talk!

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:19):

it's the prod cross

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:19):

which cross are you talking about?

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

view this post on Zulip Kenny Lau (Mar 11 2019 at 22:20):

\X was ⨯ (U+2A2F), and now \x is × (U+00D7)

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

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:20):

why are you using notations like this?

view this post on Zulip Kenny Lau (Mar 11 2019 at 22:21):

⨯ (U+2A2F) is not found in mathlib

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

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:21):

I would suggest reinstating it as \cross

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:22):

this is underhanded lean

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

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:24):

How can I get a reasonable symbol for prod.map then?

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:24):

<×>?

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:25):

reasonable?

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:25):

I'm not a fan of this crazy unicode overloading

view this post on Zulip Mario Carneiro (Mar 11 2019 at 22:25):

it makes it very difficult to read and know what's what

view this post on Zulip Patrick Massot (Mar 11 2019 at 22:25):

This is only a workaround until we get the Parser.

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

view this post on Zulip Patrick Massot (Mar 12 2019 at 14:50):

I vote for getting it back

view this post on Zulip Edward Ayers (Mar 12 2019 at 14:51):

Quick fix -- add this to your settings file:

"lean.input.customTranslations": {
  "X" : "\u2A2F"
}

view this post on Zulip 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.
· • . ․ ‧ ⋅ ⬝ ∙ ● ⚫ ⬤ 🌑

view this post on Zulip Edward Ayers (Mar 12 2019 at 14:57):

⁃ ∎ ╸ ╹ ╺ ╻ ━ ■ ▪ ▬ ▮ ◼ ◾ ⬛ ⯀ 🔲

view this post on Zulip Edward Ayers (Mar 12 2019 at 14:58):

⋄ ◇ ◊ ♢ ✧ ⬦ ⬨ ⬫

view this post on Zulip Edward Ayers (Mar 12 2019 at 14:58):

‣ ▶ ▸ ▸ ⯈ 🢒

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:01):

I'm pretty sure we can put that third line to good use

view this post on Zulip Patrick Massot (Mar 12 2019 at 15:02):

I notice that nobody complained about that cross during my Amsterdam talk


Last updated: May 14 2021 at 03:27 UTC