diff --git a/vscode-lean4/manual/manual.md b/vscode-lean4/manual/manual.md index 284ad816..5197ddf4 100644 --- a/vscode-lean4/manual/manual.md +++ b/vscode-lean4/manual/manual.md @@ -213,7 +213,7 @@ Lean code uses lots of [Unicode symbols](https://home.unicode.org/) to aid reada To replace an abbreviation early, before it is complete, `Tab` can be pressed to trigger the ['Input: Convert Current Abbreviation'](command:lean4.input.convert) command. This will yield the Unicode symbol with the shortest abbreviation identifier matching the identifier that was typed. Abbreviations are also replaced early when the text cursor is moved away from the abbreviation. -The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. +The full list of supported abbreviation identifiers and Unicode symbols can be viewed using the ['Docs: Show Unicode Input Abbreviations'](command:lean4.docs.showAbbreviations) command that can be found in the 'Documentation…' submenu of the command menu. When encountering a Unicode symbol in Lean code, [hovering](#hovers) over the symbol will also provide all available abbreviation identifiers to input the symbol. If you wish to add new abbreviations or modify existing abbreviations, please first discuss it on [Zulip](https://leanprover.zulipchat.com/), and then make a PR to modify [vscode-lean4/lean4-unicode-input/src/abbreviations.json](https://github.com/leanprover/vscode-lean4/blob/master/lean4-unicode-input/src/abbreviations.json). For some Unicode brackets, there are special abbreviation identifiers that also insert a matching closing Unicode bracket and ensure that the cursor is in-between the Unicode brackets after replacing the abbreviation. For example, `\<>` yields `⟨⟩`, `\[[]]` yields `⟦⟧`, `\f<<>>` yields `«»` and `\norm` yields `‖‖`.