Edit symbol shortcuts

Stream: general

[Peter Nelson]

How do I change or add to the list of escape sequences for unicode symbols in VScode?

[Kevin Buzzard]

The relevant global file is here but AFAIK you have to make a PR and then wait for someone to release a new version of the lean plugin. Is there a way to make changes locally?

I love browsing that file BTW.

def Ϡ : ℕ := 37 -- works fine

[Peter Nelson]

I'm sure I figured out how to do this two years ago, but can't find it searching on zulip

[Floris van Doorn]

Go to settings (ctrl+,) and search for Lean input custom translations. You can add manual shortcuts yourself there.

[Peter Nelson]

Thank you!

[Tomas Skrivan]

Here is how you do it in Emacs. Put this somewhere in your config file

(require 'lean4-input)
(push '("pd"  . ("∂")) lean4-input-user-translations)
(lean4-input-setup)

[Julian Berman]

If we're leaving breadcrumbs for future searchers :), in neovim, the setting is abbreviations.extra, i.e. --

require('lean').setup{
  abbreviations = {
    extra = {
      -- Add a \wknight abbreviation to insert ♘
      wknight = '♘',
    },
  },
}