List of custom syntax

Stream: general

[Sabrina Jewson]

Is there a list anywhere of all the custom syntax introduced by Core, Std, and Mathlib? I would like to configure my OS keyboard settings so I can type them all even outside of a text editor.

[Mario Carneiro]

I think #help term should show most of them

[Kevin Buzzard]

@Eric Wieser once posted how to do this configuring for OS = Android and it really upped my game for Zulip messages on my mobile :-) (unfortunately now I have a new phone so back to the drawing board...)

[Eric Wieser]

The thread is here, but that dictionary is very out-dated and it would be better to regenerate it before installing it

[Kevin Buzzard]

Oh -- probably worth remarking that this wasn't done via looking at all the custom syntax introduced by the Lean code but rather by the shortcuts allowed in the VS Code extension which you can see here.

[Sabrina Jewson]

Mario Carneiro said:

I think #help term should show most of them

Ah, thank you!

[Mario Carneiro]

note, it doesn't show local or scoped notations which are not enabled

[Mario Carneiro]

or things in categories other than term (but see also #help attr, #help tactic, #help conv for the others)

[Mario Carneiro]

grepping the mathlib source is probably a more complete way to find everything used in mathlib in any context

[Mario Carneiro]

and I'm almost certain that any special character that appears in lean core also appears somewhere in mathlib

[Siddhartha Gadgil]

In case it is useful:

As data for help with translations, I extracted term syntax with examples at
https://github.com/siddhartha-gadgil/LeanAide/blob/main/data/term-kinds.json

I have not figured our how to do this with, for example, BigOperators open.