Zulip Chat Archive
Stream: general
Topic: norm notation
Eric Wieser (Nov 17 2022 at 07:50):
the characters we use for norms and "parallel" are swapped from what Unicode descriptions would make the most appropriate characters for those purposes.
This strikes me as an accident we should just fix
Eric Wieser (Nov 17 2022 at 07:52):
Especially given how parallel renders in some fonts:
This is probably ok for parallel, but is deeply weird for norm.
Eric Wieser (Nov 17 2022 at 08:03):
I'll make a start on a patch (edit: done at #17575)
Yaël Dillies (Nov 17 2022 at 10:37):
Can you swap the VScode extension abbreviations as well? I'm used to \|| meaning "norm".
Eric Wieser (Nov 17 2022 at 10:50):
See the comment on the PR; There's a \norm shortcut waiting to be merged that is shorter than \||\|| anyway. If we changed \|| then \||n would be weird since that means "not parallel" not "double bar with strike"
Eric Wieser (Nov 17 2022 at 10:51):
CI is green on #17575; while it's trivial to fixup, I imagine it will go stale quite quickly
Sebastien Gouezel (Nov 17 2022 at 10:57):
I'd really like to have \||to default to the norm symbol, because it's used much more than the parallel one.
Eric Wieser (Nov 17 2022 at 10:58):
Is there any reason to type \||x\|| over \norm x though?
Sebastien Gouezel (Nov 17 2022 at 10:58):
(And there are conflicts on the PR).
Sebastien Gouezel (Nov 17 2022 at 10:59):
Just a habit it will be hard to get rid off. And this corresponds to latex notation.
Eric Wieser (Nov 17 2022 at 10:59):
Isn't the latex notation \|, which already means the wrong thing in vscode?
Sebastien Gouezel (Nov 17 2022 at 11:00):
In fact I'm not sure, because I use \norm{x} in latex :-)
Eric Wieser (Nov 17 2022 at 11:02):
Either way, I probably should let someone who uses norm more argue about this; the extent of my counterargument is that we have a lot of shortcuts similar to \|| that are about the geometry symbols, and it would be odd to mix a norm symbol with them. Likely we don't care about that
Sebastien Gouezel (Nov 17 2022 at 11:18):
I guess norm is used 10 times more in mathlib than all the other geometry symbols together. So it really deserves its own shortcut like \|| in addition to \norm.
Notification Bot (Nov 17 2022 at 11:20):
17 messages were moved here from #mathlib4 > => notation by Eric Wieser.
Eric Wieser (Nov 17 2022 at 11:23):
For reference, the PR adding \norm is https://github.com/leanprover/vscode-lean/pull/315
Eric Wieser (Nov 17 2022 at 11:24):
Which I think only @Gabriel Ebner has permission to merge/enable CI/accept suggested changes on
Jireh Loreaux (Nov 17 2022 at 14:01):
I much prefer to type \norm over \|| and I would be content if the latter were the way to type parallel, but I'm obviously biased because I'm the one who wrote the PR adding \norm.
Eric Wieser (Nov 17 2022 at 15:42):
Would you mind accepting my suggested changes on your PR @Jireh Loreaux? The change to mathlib is almost in master
Floris van Doorn (Nov 17 2022 at 16:25):
I opened leanprover/vscode-lean#319
Eric Wieser (Nov 17 2022 at 16:34):
Wait, what is fuzzy (docs#fuzzy) and did I change it by accident? (edit: introduced here)
Eric Wieser (Nov 17 2022 at 16:36):
Hmm, maybe that one _should_ be \parallel. I foolishly assumed that @Joseph Myers's list was exhaustive...
Yuyang Zhao (Nov 17 2022 at 16:43):
Wikipedia uses║ for fuzzy and I think it should be vertical lines too.
Eric Wieser (Nov 17 2022 at 16:55):
That's U+2551 Box Drawings ║ which is different again (and was contributed in 2007 in https://en.wikipedia.org/w/index.php?title=Fuzzy_game&diff=prev&oldid=111701737)
Eric Wieser (Nov 17 2022 at 16:59):
@Violeta Hernández; since you added the notation, do you care either way?
Yuyang Zhao (Nov 17 2022 at 17:02):
(I haven't seen her online for a very long time)
Yuyang Zhao (Nov 17 2022 at 17:03):
Oh zulip can send an email, nvmd.
Violeta Hernández (Nov 17 2022 at 17:05):
I haven't been online for a very long time
Violeta Hernández (Nov 17 2022 at 17:05):
But no, I don't mind either way
Floris van Doorn (Nov 17 2022 at 17:30):
I'm happy to change the symbol for fuzzy, as long as the VS-code abbreviation and the mathlib symbol match.
Eric Wieser (Nov 17 2022 at 18:05):
Let's leave it as is (ie, as the version I accidentally changed it to), I doubt it really matters, and there are very few people who will be impacted by the change anyway
Joseph Myers (Nov 17 2022 at 19:45):
I mentioned fuzzy in #16298, but I'm not at all surprised that there's a fifth double-vertical-line Unicode character beyond the ones I identified there.
María Inés de Frutos Fernández (Nov 29 2022 at 09:50):
Eric Wieser said:
For reference, the PR adding
\normis https://github.com/leanprover/vscode-lean/pull/315
The \norm shortcut is not working for me, do I need to install/update anything to have it available?
Eric Wieser (Nov 29 2022 at 09:59):
I think we need to ask @Gabriel Ebner nicely to make a release :)
Eric Wieser (Nov 29 2022 at 11:06):
Maybe with https://github.com/leanprover/vscode-lean/pull/322 in first...
Eric Wieser (Jan 08 2023 at 14:29):
@Gabriel Ebner, would you be able to make this release sometime next week?
Gabriel Ebner (Jan 10 2023 at 01:58):
Thanks for pinging me!
Last updated: Dec 20 2023 at 11:08 UTC