Zulip Chat Archive

Stream: general

Topic: I need a list of all `\nat` shortcut strings


Daniel Donnelly (May 09 2021 at 08:29):

Here is a screenshot of what I'm working on:

image.png

I would like a list of all \shortcut_string codes used with Lean. I don't know if I'll make it into a Lean Editor, since I want to experiment with type theory, but was just wondering, since lean has a double-struck ZZ in its documentation. But it doesn't say how to enter it just like \nat for the natural numbers.

Thank you!

Patrick Massot (May 09 2021 at 08:33):

Are you asking for https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json?

Daniel Donnelly (May 09 2021 at 08:35):

@Patrick Massot yes, that is amazing ! :D It's even in the right format for a Python dictionary :)

That's thousands, lol. I think I only want to use maybe 50 of them. You really over-provided me with the correct answer.


Last updated: Dec 20 2023 at 11:08 UTC