Zulip Chat Archive

Stream: new members

Topic: dagger symbol displayed as emoji?

Klaus Gy (Jul 04 2023 at 13:01):

what does the dagger symbol :cross: mean? from what i gathered, something like inaccessible term, but i didnt find it in the documentation? also in the vscode mouseovers it displays the emoji :cross: instead of the normal † (the first one is displayed as a white dagger in a purple box to me, the second one as standard symbol). is this a problem with my fonts? also when you google leanprover "✝" you find a lot of hits...

Patrick Massot (Jul 04 2023 at 13:04):

It means "inaccessible object". You can't refer to it directly. It usually mean you didn't provide a name for it. Lean came up with a name but doesn't want you to rely on it.

Patrick Massot (Jul 04 2023 at 13:05):

There is some discussion a bit hidden at https://leanprover.github.io/lean4/doc/examples/tc.lean.html?highlight=inaccessible#a-certified-type-checker

Klaus Gy (Jul 04 2023 at 13:13):

thank you! but i dont see the dagger on that page? in the page before, they say ‹e› is used as sytactic sugar for inaccessible names, is this the same? and do you see the emoji or the normal dagger in e.g. vscode mouseovers?

Klaus Gy (Jul 04 2023 at 13:15):

this is how it looks like to me, is this intended?

Patrick Massot (Jul 04 2023 at 13:29):

In the page I linked to, you are looking for the word "inaccessible". And you can see daggers if you put your mouse cursor over the small ovals in the code snippets.

Patrick Massot (Jul 04 2023 at 13:30):

I never see the purple dagger from your picture.

Matthew Ballard (Jul 04 2023 at 13:49):

Is this emacs?

Klaus Gy (Jul 05 2023 at 14:24):

apparently a lot of browsers display this as emoji, see here: https://stackoverflow.com/questions/32915485/how-to-prevent-unicode-characters-from-rendering-as-emoji-in-html-from-javascrip

Klaus Gy (Jul 05 2023 at 14:25):

thats unfortunate for those of us who use vscode in the browser :(

Klaus Gy (Jul 05 2023 at 14:25):

Matthew Ballard said:

Is this emacs?

no, thats just my browser

Klaus Gy (Jul 05 2023 at 14:27):

is it important that latin cross is used here and not dagger? can i file an issue to change the latin cross to dagger for better compatibility?

Patrick Massot (Jul 05 2023 at 14:42):

The semantic really isn't the same. We want a tomb stone here.

Klaus Gy (Jul 05 2023 at 14:44):

but its not a tomb stone for all users

Klaus Gy (Jul 05 2023 at 14:45):

if you want it to display as emoji for everyone, you could use an variation selector, but none is present

Klaus Gy (Jul 05 2023 at 14:49):

right now lean uses the unicode symbol "latin cross" which should render very similar to dagger (without variation selector present), but some browsers incorrectly render it as emoji

Klaus Gy (Jul 05 2023 at 14:50):

here is the corresponding line in leans source code: https://github.com/leanprover/lean4/blob/5402c3cf76eb1ef470954d15ced317c65e13d05a/src/Lean/Hygiene.lean#L49

Patrick Massot (Jul 05 2023 at 14:53):

Actually https://en.wikipedia.org/wiki/Dagger_(mark) claims dagger also means death, so maybe this is a good choice.

Patrick Massot (Jul 05 2023 at 14:53):

@Sebastian Ullrich?

Sebastian Ullrich (Jul 05 2023 at 14:56):

More commonly though it represents a footnote, which I don't think is a helpful association here

Klaus Gy (Jul 05 2023 at 15:02):

this is what it looks like to me, like i said, this is basically a browser bug, but it seems like a lot of browsers are doing this, i kinda dont like the aeesthetics of emojis in code :/

Klaus Gy (Jul 05 2023 at 15:03):

you could add the variation selector vs15 to tell the browser/editor to display it as non-emoji glyph, but most browsers just ignore it as well :/

Klaus Gy (Jul 05 2023 at 15:59):

heavy latin cross would also be available, it has no emoji counterpart: https://www.compart.com/en/unicode/U+1F547

Last updated: Dec 20 2023 at 11:08 UTC