This is also how it works in Lean and in VSCode with the Lean extension it will also show you overlay saying how to type the symbol if you are unfamiliar with i

This is also how it works in Lean and in VSCode with the Lean extension it will also show you overlay saying how to type the symbol if you are unfamiliar with it. I'm not sure who came up with this feature first but it seems emacs has something similar so it probably came from there. (Edit: Someone else here thinks it originated in Plan 9) It works quite well. However, there is still a room for improvement: 1. Like was mentioned elsewhere in this thread on copy we could convert the symbol to how it is typed in order to support text (or even ASCII) only tools. 2. Better Integration with the browser and development tools like git so they get prettified when possible.