Commit 76727db
authored
fix Tilde and RawTilde (#45)
\[Tilde] is a character associated to the unicode \u223c instead of ~
\[Tilde] is an operator which is not Infix but Tilde, with precedence 290.
\[Tilde] has a wl-unicode-name TILDE OPERATOR
~ is not a valid ASCII representation for this operator (otherwise, the conversion get broken)
\[RawTilde] is the (ASCII) character ~, and it is associated to Infix, and is associated to the wl-unicode character ~ and
wl-unicode-name TILDE1 parent be4d6de commit 76727db
1 file changed
+8
-6
lines changed| Original file line number | Diff line number | Diff line change | |
|---|---|---|---|
| |||
4469 | 4469 | | |
4470 | 4470 | | |
4471 | 4471 | | |
4472 | | - | |
| 4472 | + | |
4473 | 4473 | | |
4474 | 4474 | | |
4475 | 4475 | | |
4476 | 4476 | | |
4477 | 4477 | | |
4478 | 4478 | | |
4479 | 4479 | | |
4480 | | - | |
4481 | 4480 | | |
4482 | 4481 | | |
4483 | 4482 | | |
| |||
6221 | 6220 | | |
6222 | 6221 | | |
6223 | 6222 | | |
| 6223 | + | |
| 6224 | + | |
6224 | 6225 | | |
6225 | 6226 | | |
6226 | 6227 | | |
| |||
7563 | 7564 | | |
7564 | 7565 | | |
7565 | 7566 | | |
7566 | | - | |
| 7567 | + | |
7567 | 7568 | | |
7568 | 7569 | | |
7569 | | - | |
7570 | 7570 | | |
7571 | 7571 | | |
7572 | 7572 | | |
7573 | 7573 | | |
| 7574 | + | |
7574 | 7575 | | |
7575 | | - | |
7576 | | - | |
| 7576 | + | |
| 7577 | + | |
| 7578 | + | |
7577 | 7579 | | |
7578 | 7580 | | |
7579 | 7581 | | |
| |||
0 commit comments