Add aliases for the symbols ⩵, ⩶, ⩽, ⩾, etc.

[BenjaminGalliot]

For the symbols ⩵ and ⩶, as aliases for == and ===, this would standardize these operators with single-character (Unicode) symbols, to complete the list alongside ≠, <, >, ≤, ≥, etc. This is related to this Discourse topic.

For the symbols ⩽ and ⩾, besides the fact that they are supposed to be equivalent to ≤ and ≥, depending on the country (see in particular this link), and that they are used in this reference document, some keyboard layouts directly have the symbols ⩽ & ⩾ and not ≤ & ≥ (such as the French Bépo-AFNOR).

I don't know if I should go up to the − (currently invalid) and × symbols (they are directly accessible in some layouts) – knowing that ÷ already has its own purpose –, but everything is open for discussion. Same goes for … as alias for ..., but it is trickier here because it is not a function identifier…

There may be other symbols in this case that I haven't thought of, feel free to bring them up!

The goal is not to limit the number of free symbols that users can use, but to correct some inconsistencies that may date while making the code easier to read or write for a non-negligible part of the users...

I would point out that some users type LaTeX commands to write them while others have custom keyboard layouts to get them directly.

I know this may create conflicts for already existing modules (small breaking change) that might use these symbols for other purposes (I think this must be rare for ⩵, ⩶, ⩽ and ⩾) so it needs to be considered, and we can prepare this change with temporary warnings…

[Seelengrab]

These types of ligatures should be limited to how an editor renders the text, in my opinion. The core constructs they represent should always be displayable, even if the font used for rendering does not support those UTF-8 characters.

[StefanKarpinski]

I'm fine with having these since it seems like a reasonable default for ⩵ and ⩶ to mean == and ⩶, respectively. After all, it's not like we're going to give them some other meaning, so why not? Note that they can still be given a different meaning if someone wants to, which someone brought up in that thread as an attack vector, but you can already reassign == and === so this is certainly no worse.

[petar]

The Lean Theorem Prover language has done a great job with incorporating unicode symbols in the language, together with escape sequence support in their vscode extension. Having parity with Lean seems like a good goal, as both of these languages are currently the defacto standard for academic mathematics in their respective domains.

[StefanKarpinski]

Yeah, we're fine with it, someone just needs to make the actual change.

[StefanKarpinski]

I agree with @Seelengrab that the ligature approach is preferable, but if these characters do occur in code, why not let them work? It's pretty perverse to have ⩶ mean anything besides ===, after all.

[BenjaminGalliot]

I started a PR, and added Unicode equivalents for all the operators I mentioned in my first post (except for …). Let me know if there are any cases that are more debatable, and of course if I've missed any lines or made some errors...

I was facing a small choice... What could be the ideal negation of ⩶: !⩵ or !⩶ (truncation of the operator as for !=/== or just addition of ! in front)? For the moment, I've put both as equivalent.

In the same way, should we also define the following operators: ≮, ≯, ≰ and ≱?

[BenjaminGalliot]

So I finally opened my PR for revision. I just added the last 4 operators and their Fix2 functions.

We should keep this issue open for discussion on other operators or symbols.

[BenjaminGalliot]

I saw on version 1.7 some additions about operators. Should we try to continue the review of #41787?