-
-
Notifications
You must be signed in to change notification settings - Fork 5.5k
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
Add \bbsemi as a binary operator #34722
Conversation
Formal Specification— Z Notation— Syntax, Type and Semantics (http://www.open-std.org/jtc1/sc22/open/n3187.pdf) says
( The motivation discussed in the aforementioned discourse thread was to define As two characters are pretty much identical, I think omitting schema composition (2A1F) makes sense. This is compatible with that we don't have, e.g., Another consideration may be to see if there are fonts that have only one of the characters. But so far I find that it's either both of them are rendered or none of them are rendered (though maybe it's just my editor and terminal are finding fallbacks). |
From simple inspection of the unicode alternatives at this page https://unicode.org/charts/PDF/U2A00.pdf I find 2A1F much more appealing visually (compared to its counterpart 2A3E). In addition, also its latex name is lovely self-descriptive |
It seems there are multiple ways to enter certain symbols. So I hope it's OK to add both julia> length(unique(keys(REPL.REPLCompletions.latex_symbols)))
2495
julia> length(unique(values(REPL.REPLCompletions.latex_symbols)))
2475 Re: 2A3E vs 2A1F, I don't really mind which one is chosen. It looks like 2A1F is rendered as a bigger symbol so maybe it's better for readability. |
I think |
I replaced Can this be merged? Is there anything else to be addressed? |
I removed Note that people want to use this alias can simply do: julia> using REPL
julia> REPL.REPLCompletions.latex_symbols["\\fatsemi"] = "⨟" |
;
is used as the composition operator in "diagrammatic order" (Category (mathematics) - Wikipedia). Although we can't use the normal semicolon as a binary operator in Julia, we can include⨟
(\fatsemi
) as a binary operator.A big thanks to the post by @schlichtanders in Discourse: https://discourse.julialang.org/t/add-composition-operator-unicode-2a1f-for-flipped/34436