Zulip Chat Archive

Stream: general

Topic: Notation for `mv_polynomial`?

Yury G. Kudryashov (Dec 23 2021 at 00:09):

What do you think about notation R［σ］ for mv_polynomial σ R? These are fullwidth left/right square brackets.

Adam Topaz (Dec 23 2021 at 01:20):

LGTM!

Yury G. Kudryashov (Dec 23 2021 at 03:06):

What hotkey should we use for these symbols? How do I PR hotkeys for VS code lean input mode?

Johan Commelin (Dec 23 2021 at 06:44):

@Yury G. Kudryashov https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

Last updated: Dec 20 2023 at 11:08 UTC