dagger symbol displayed as emoji?

Stream: new members

[Klaus Gy]

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]

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]

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]

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]

image.png
this is how it looks like to me, is this intended?

[Patrick Massot]

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]

I never see the purple dagger from your picture.

[Matthew Ballard]

Is this emacs?

[Klaus Gy]

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]

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

[Klaus Gy]

Matthew Ballard said:

Is this emacs?

no, thats just my browser

[Klaus Gy]

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]

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

[Klaus Gy]

but its not a tomb stone for all users

[Klaus Gy]

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

[Klaus Gy]

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]

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

[Patrick Massot]

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

[Patrick Massot]

@Sebastian Ullrich?

[Sebastian Ullrich]

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

[Klaus Gy]

image.png
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]

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]

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