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

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

Last updated: May 08 2021 at 03:17 UTC