Repository navigation
Add ↔︎ with text variation selector as a notation for equivalence. - #311
Merged
Merged
Conversation
proux01
reviewed
Oct 14, 2026
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
proux01
reviewed
Oct 15, 2026
Contributor
|
Do we really want to do this? When is it actually a problem? Would it need doing for every symbol? |
Co-authored-by: Pierre Roux <pierre.roux@onera.fr>
Contributor
Author
|
It is a problem if a user writes the arrow with the variation selector, which is a valid representation of the symbol w.r.t. the Unicode chart, yet it is currently rejected by the parser if we keep only the first notation. |
Contributor
|
Thanks for the explanation. Then let's merge this and you can open a further PR if you want to change the printing (will require an overlay in stdpp). |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR aims at adding the ↔︎ (represented in UTF-8 by the sequence of bytes 0xE2 0x86 0x94 0xEF 0xB8 0x8E) symbol, which is the unicode codepoint for the double-sided arrow ↔ (bytes 0xE2 0x86 0x94) followed by the text variation selector (bytes 0xEF 0xB8 0x8E), forcing it to be displayed as text and not as the corresponding emoji (↔ followed by the emoji variation selector (0xEF 0xB8 0x8F) is displayed as↔️ ).
Therefore, 0xE2 0x86 0x94 0xEF 0xB8 0x8E and 0xE2 0x86 0x94 are two valid way to represent ↔ in UTF-8, but only the latter is recognized by Rocq's notations, this PR adds the former too.