This is a guide to map combinations of characters to Unicode mathematical symbols.
The original inspiration is the incredibly useful gist by Andrej Bauer, and this gist aims to extend the idea to lower / upper case key combinations. This is achieved by using .cin
input maps, originally developed to quickly insert Chinese characters, to encode a wide range of math symbols.
The method is expressive enough to encode almost all shortcuts from the keymap used by the Lean 4 plugin in Visual Studio Code.
- Download the
lean4.cin
file from this repository or generate an up-to-date version by running thegenerate_cin.py
script. Don't copy-paste it from the browser because the file must be inUTF-8
encoding.