Zulip Chat Archive

Stream: PR reviews

Topic: 3212 compl notation


view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 21:48):

#3212 touches 41 files, so I think that we should merge it before it rots.

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 21:49):

I understand that it's long but it's only about changing - to \C or \

view this post on Zulip Patrick Massot (Jun 28 2020 at 21:50):

Crap, I see this one minute too late.

view this post on Zulip Patrick Massot (Jun 28 2020 at 21:51):

I just sent Heine to the queue since Sébastien bors d+ed it. And it does use complement with the stupid old notation.

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 21:52):

OK, I'll merge staging and fix notation.

view this post on Zulip Patrick Massot (Jun 28 2020 at 21:52):

Note that this Heine PR touches only one file.

view this post on Zulip Patrick Massot (Jun 28 2020 at 21:56):

I have a question actually. Do we want this space after the C? Bourbaki doesn't has a space here. I checked and the Lean parser doesn't mind.

view this post on Zulip Yury G. Kudryashov (Jun 28 2020 at 22:05):

I don't care. Should I sed remove the space?

view this post on Zulip Patrick Massot (Jun 28 2020 at 22:10):

I don't know actually. I wish this symbol would be as recognizable as in Bourbaki where it's both taller and bolder (I don't like that it is bold in Bourbaki, but tall is nice).

view this post on Zulip Patrick Massot (Jun 28 2020 at 22:11):

And I need to sleep, so I'll let everybody else decide.

view this post on Zulip Johan Commelin (Jun 29 2020 at 03:48):

Are there unicode variations that are easier to distinguish from a recular C?

view this post on Zulip Johan Commelin (Jun 29 2020 at 03:53):

Another option migth be a superscript c as postfix notation. Something like Xᶜ
Is https://en.wikipedia.org/wiki/Stretched_C the thing you are currently using?

view this post on Zulip Johan Commelin (Jun 29 2020 at 03:55):

Aha, there is a dedicated "Complement" symbol in Unicode, which is what Yury has been using so far, it looks like: .
There is also the "Stretched C", which looks like ʗ.

view this post on Zulip Johan Commelin (Jun 29 2020 at 03:57):

I understand that it is technically better to use "Complement". But from a UX point of view, it seems too easy to confuse it for a regular "C".

view this post on Zulip Patrick Massot (Jun 29 2020 at 07:31):

In the font I'm using in VSCode, "Stretched C" is much more recognizable that "Complement", and much closer to Bourbaki's notation.

view this post on Zulip Patrick Massot (Jun 29 2020 at 07:32):

I vote for switching to streched C without space and merging.

view this post on Zulip Patrick Massot (Jun 29 2020 at 07:35):

This will probably need a PR to VScode translations then.

view this post on Zulip Scott Morrison (Jun 29 2020 at 08:23):

That looks good in my VSCode too.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 15:44):

Which font do you use? In "Hack" ʗ is shifted down w.r.t. the baseline.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 15:45):

BTW, can we use a proper unicode symbol and adjust highlighting in VScode/Emacs?

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 15:46):

E.g., make it bold.

view this post on Zulip Floris van Doorn (Jun 29 2020 at 15:53):

I would prefer a different notation for complementation. I think a postfix superscript c is pretty common: . This could also be the notation for complement in a boolean algebra.

view this post on Zulip Sebastien Gouezel (Jun 29 2020 at 15:58):

The ʗ looks ugly with my (default) font, and is by far less standard than the postfix superscript c in papers I have read by non-French writers.

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 15:58):

Could you please write the notation line?

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 15:58):

∁ʗᶜ

view this post on Zulip Patrick Massot (Jun 29 2020 at 16:01):

I would be fine with the postfix upper c.

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:06):

postfix ``:(max+1) := set.compl

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:06):

I can add the character to the VSCode input list (currently you cannot input it with \^c).

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:07):

With this precedence f sᶜ is parsed as f (sᶜ), which I think is what we want.

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:08):

\^c is good, but also \compl please

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:09):

Of course!

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:15):

leanprover/vscode-lean#196

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 16:16):

You can input it with \^c in Emacs lean-mode

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:16):

Oh good!

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:16):

Could you double check that it is indeed the same character?

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 16:18):

Done.

view this post on Zulip Floris van Doorn (Jun 29 2020 at 16:32):

I also filed leanprover-community/lean#367

view this post on Zulip Johan Commelin (Jun 29 2020 at 16:32):

(aka lean#367 :wink:)

view this post on Zulip Yury G. Kudryashov (Jun 29 2020 at 17:04):

I'm recompiling with the new notation.


Last updated: May 09 2021 at 14:10 UTC