These code snippets allow the insertion of unicode symbols from the corresponding LaTeX commands. When editing a plaintext file, it provides autocompletions for LaTeX symbols, which are triggered on \.
The list of symbols is currently generated from the Coq Integrated Development Environment LaTeX-to-unicode tool, using this script.
To install, copy the file with extension .code-snippets in the user snippets folder (see the Visual Studio Code user guide).
To regenerate the snippets, use the Makefile.