Zulip Chat Archive

Stream: new members

Topic: Abbreviation


view this post on Zulip Nicolò Cavalleri (Aug 07 2020 at 14:30):

Is there a list somewhere of abbreviations in Lean introduced by the backslash such as \smul?

view this post on Zulip Shing Tak Lam (Aug 07 2020 at 14:30):

https://github.com/leanprover/vscode-lean/blob/master/translations.json

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Nicolò Cavalleri (Aug 07 2020 at 14:33):

I thought they were specific to lean

view this post on Zulip Patrick Massot (Aug 07 2020 at 14:33):

It's specific to the Lean extension for VSCode.

view this post on Zulip Patrick Massot (Aug 07 2020 at 14:33):

as you can see from the url above

view this post on Zulip Nicolò Cavalleri (Aug 07 2020 at 14:34):

Ok thanks

view this post on Zulip Patrick Massot (Aug 07 2020 at 14:40):

Note this is not only pedantry because some people use Lean in emacs.

view this post on Zulip Mario Carneiro (Aug 07 2020 at 14:43):

Emacs also has a list like this though

view this post on Zulip Patrick Massot (Aug 07 2020 at 14:43):

Sure, but I think they are not exactly the same.

view this post on Zulip 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