As mentioned in another question, the way that VSCode and other editors implement unicode characters that cannot be typed directly from most keyboards is an editor feature.

As such, different editors could do it differently, so that for instance, $\varphi$ and $\phi$ could be entered as \varphi, \phi, the other way around, or something else.

But perhaps there is still an official recommendation on how editors should let you type unicode characters; or was a choice made to not make an official recommendation?

  • $\begingroup$ Maybe agda-mode $\endgroup$
    – ice1000
    Commented Feb 10, 2022 at 1:09
  • $\begingroup$ Iirc you can use an unsubstituted \l or \R in Lean source code, so I imagine the list probably comes from somewhere official. $\endgroup$
    – wizzwizz4
    Commented Feb 10, 2022 at 1:14

1 Answer 1


Because maintaining such a big list of Unicode abbreviations is annoying and none of the editor mode maintainers are interested in encouraging untransferrable abbreviations, as far as I know, all of the Lean editor modes just copy the abbreviations.json file (the VS Code plugin is the most popular, so new abbreviations usually land there first). In practice I haven't heard of divergence between editor abbreviations files ever being an issue.

So to the extent that there is an "official recommendation" to use the VS Code plugin for Lean, that comes with the bundled list of abbreviations, but users can also add their own abbreviations if they want.

  • $\begingroup$ lean-mode, from which abbreviations.js was first derived, doesn't use it (and is not fully synchronized with it afaik). The list in lean-mode in turn was derived from agda-mode's. But abbreviations.js is very much the authoritative source now, yes. $\endgroup$ Commented Feb 10, 2022 at 9:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.