Zulip Chat Archive
Stream: PR reviews
Topic: 3212 compl notation
Yury G. Kudryashov (Jun 28 2020 at 21:48):
#3212 touches 41 files, so I think that we should merge it before it rots.
Yury G. Kudryashov (Jun 28 2020 at 21:49):
I understand that it's long but it's only about changing - to \C or \
Patrick Massot (Jun 28 2020 at 21:50):
Crap, I see this one minute too late.
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.
Yury G. Kudryashov (Jun 28 2020 at 21:52):
OK, I'll merge staging and fix notation.
Patrick Massot (Jun 28 2020 at 21:52):
Note that this Heine PR touches only one file.
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.
Yury G. Kudryashov (Jun 28 2020 at 22:05):
I don't care. Should I sed remove the space?
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).
Patrick Massot (Jun 28 2020 at 22:11):
And I need to sleep, so I'll let everybody else decide.
Johan Commelin (Jun 29 2020 at 03:48):
Are there unicode variations that are easier to distinguish from a recular C?
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?
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 ʗ.
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".
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.
Patrick Massot (Jun 29 2020 at 07:32):
I vote for switching to streched C without space and merging.
Patrick Massot (Jun 29 2020 at 07:35):
This will probably need a PR to VScode translations then.
Scott Morrison (Jun 29 2020 at 08:23):
That looks good in my VSCode too.
Yury G. Kudryashov (Jun 29 2020 at 15:44):
Which font do you use? In "Hack" ʗ is shifted down w.r.t. the baseline.
Yury G. Kudryashov (Jun 29 2020 at 15:45):
BTW, can we use a proper unicode symbol and adjust highlighting in VScode/Emacs?
Yury G. Kudryashov (Jun 29 2020 at 15:46):
E.g., make it bold.
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.
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.
Yury G. Kudryashov (Jun 29 2020 at 15:58):
Could you please write the notation line?
Yury G. Kudryashov (Jun 29 2020 at 15:58):
∁ʗᶜ
Patrick Massot (Jun 29 2020 at 16:01):
I would be fine with the postfix upper c.
Floris van Doorn (Jun 29 2020 at 16:06):
postfix `ᶜ`:(max+1) := set.compl
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).
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.
Johan Commelin (Jun 29 2020 at 16:08):
\^c is good, but also \compl please
Floris van Doorn (Jun 29 2020 at 16:09):
Of course!
Floris van Doorn (Jun 29 2020 at 16:15):
Yury G. Kudryashov (Jun 29 2020 at 16:16):
You can input it with \^c in Emacs lean-mode
Floris van Doorn (Jun 29 2020 at 16:16):
Oh good!
Floris van Doorn (Jun 29 2020 at 16:16):
Could you double check that it is indeed the same character?
Yury G. Kudryashov (Jun 29 2020 at 16:18):
Done.
Floris van Doorn (Jun 29 2020 at 16:32):
I also filed leanprover-community/lean#367
Johan Commelin (Jun 29 2020 at 16:32):
(aka lean#367 :wink:)
Yury G. Kudryashov (Jun 29 2020 at 17:04):
I'm recompiling with the new notation.
Last updated: Dec 20 2023 at 11:08 UTC