Unicode Tables for VSCode

Stream: general

[Jineon Baek]

In VSCode, you can type backslash \ then some sequence of alphabet characters to type a unicode. e.g. \in to type ∈.

Where are such correspondences located? I'm looking for a single table that maps \in to ∈ (and many other symbols).

[Jihoon Hyun]

They are defined here: https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json

[Julian Berman]

See https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md#unicode-input

[Julian Berman]

Specifically the Docs: Show Unicode Input Abbreviations' command