Zulip Chat Archive
Stream: new members
Topic: Abbreviation
Nicolò Cavalleri (Aug 07 2020 at 14:30):
Is there a list somewhere of abbreviations in Lean introduced by the backslash such as \smul?
Shing Tak Lam (Aug 07 2020 at 14:30):
https://github.com/leanprover/vscode-lean/blob/master/translations.json
Patrick Massot (Aug 07 2020 at 14:31):
Also note this hasn't much to do with Lean itself, this is entirely on the editor support side.
Nicolò Cavalleri (Aug 07 2020 at 14:32):
Patrick Massot said:
Also note this hasn't much to do with Lean itself, this is entirely on the editor support side.
Does \smul work for C++ as well in VSCode?
Nicolò Cavalleri (Aug 07 2020 at 14:33):
I thought they were specific to lean
Patrick Massot (Aug 07 2020 at 14:33):
It's specific to the Lean extension for VSCode.
Patrick Massot (Aug 07 2020 at 14:33):
as you can see from the url above
Nicolò Cavalleri (Aug 07 2020 at 14:34):
Ok thanks
Patrick Massot (Aug 07 2020 at 14:40):
Note this is not only pedantry because some people use Lean in emacs.
Mario Carneiro (Aug 07 2020 at 14:43):
Emacs also has a list like this though
Patrick Massot (Aug 07 2020 at 14:43):
Sure, but I think they are not exactly the same.
Mario Carneiro (Aug 07 2020 at 14:46):
https://github.com/leanprover/lean-mode/blob/master/lean-input.el
Arthur Paulino (Nov 05 2021 at 18:15):
What does abbreviation do exactly?
Kyle Miller (Nov 05 2021 at 18:17):
Last updated: Dec 20 2023 at 11:08 UTC