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.cinfile from this repository or generate an up-to-date version by running thegenerate_cin.pyscript.ย ย Don't copy-paste it from the browser because the file must be inUTF-8encoding. - Doble-click on the
lean4.cinfile in Finder to install it. The file is copied in~/Library/Input Methods/and you can check there if the file was installed correctly. - Log out and log in again to activate the new input method.
- Go to
System Preferences > Keyboard > Input Sourcesand then click on the+button to add a new input source. On the list, select 'Chinese' and then 'Lean4'. You can also search for 'Lean4' in the search bar on the bottom left. - You can now switch between the input methods by pressing
CTRL + Spaceor clicking on the input source icon on the top right of the screen.
You can customize the input method by editing the lean4.cin file. You should add one entry per line, with the format <shortcut> <symbol> (space-separated), where <shortcut> is the key combination you want to use and <symbol> is the Unicode symbol you want to output.ย ย
You can also add additional symbols during the conversion by editing the 'additional mappings'
step in the generate_cin.py script.