-
-
Notifications
You must be signed in to change notification settings - Fork 3.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Unicode Asterisk (∗) #1134
Comments
Should it look distinguishably different? |
In the other fonts that support it normal asterisk is pentagonal, while the asterisk operator is hexagonal. I think that would be a good way to keep them distinct but blend with the ligatures in a similar way. |
Ok, about ligatures. Currently |
Will be in v6 as |
maybe I got it wrong by saying "ligatures", I just care that the asterisk looks vertically centered with - or =. |
Ok I see. Will be handled in #655 |
Would be cool to have the unicode asterisk operator ∗ (U+2217) handled with the same nuance as the normal * symbol.
In particular, the same ligatures should be supported (e.g.
-∗
and=∗
).It is for example used in maths for some operators, for example for the separating conjunction in separation logics, where the normal asterisk is reserved for normal multiplication.
The text was updated successfully, but these errors were encountered: