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

Stream: general

[Daniel Donnelly]

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]

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

[Daniel Donnelly]

@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.