|
|
|
|
|
by zarzavat
620 days ago
|
|
Lean (and iirc Mathematica) use backslash escapes: you type \symbolname and the symbol is inserted by your editor. You can also imbue the backslash escape sequence with the same meaning as the unicode, so that in the event that the editor didn’t make this replacement it would still mean the same thing. |
|