Unicode symbol for `-*`

Stream: iris-lean

[Shreyas Srinivas]

Related. We should have a unicode symbol for the wand. The current ascii rendering stands out distinctly in lean code.

[Mario Carneiro]

is there a unicode wand symbol?

[Notification Bot]

2 messages were moved here from #iris-lean > Minor UX quibble by Mario Carneiro.

[Mario Carneiro]

the wand symbol is -∗ which is not actually ascii (it is -\ast)

[suhr]

P ∗ Q 🪄 Q ∗ R

[Shreyas Srinivas]

Fair point. This is the vscode symbol list for iris and I can't see one for wand in here : https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/vscode

[Mario Carneiro]

I don't think it looks that bad. I find <pers> and other modalities to be rather more distracting:
image.png

[Shreyas Srinivas]

Right. I thought □ was persistent. But apparently □ is persistent affine

[Shreyas Srinivas]

Digging into the syntax and notation setup, I wonder if we can't just use notation all the way

[Shreyas Srinivas]

We never leave the syntax category of terms anyway

[Mario Carneiro]

that's not true, iris terms are in their own syntax category

[Mario Carneiro]

No we can't use notation because iris terms are given meaning only inside iprop(_)

[Mario Carneiro]

the issue is that ∧ et al need to be interpreted differently inside iprop(_)

[Shreyas Srinivas]

Ah I just got to that point. It feels like a nice trick to never have to write a separate syntax category

[Mario Carneiro]

although now I'm wondering whether making the syntax into macros or notations will fix the issue where go to definition never works properly on iprop expressions

[Mario Carneiro]

hm, no luck