## 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?

∁ʗᶜ

#### 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

Of course!

#### Floris van Doorn (Jun 29 2020 at 16:15):

leanprover/vscode-lean#196

#### Yury G. Kudryashov (Jun 29 2020 at 16:16):

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

Oh good!

#### Floris van Doorn (Jun 29 2020 at 16:16):

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

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: May 09 2021 at 14:10 UTC