a few abbreviation changes

Stream: lean4

[Floris van Doorn]

I just made a PR vscode-lean4#422 adding a bunch of abbreviations.

There are also a few changes (I think pretty uncontroversial):

• \setminus from ∖ to \ (the latter is the ASCII symbol). The former is unused in Mathlib, except in docstrings using the symbol incorrectly to refer to the latter. The former is still available as \smallsetminus.
• \subset from ⊂ to ⊆. The former is almost unused compared to the latter in Mathlib (240 vs 6900 hits). The former symbol is still available as \ssub or \ssubset. This should also make \subs autocomplete conveniently to ⊆ instead of ⊂.
• \supset similarly from ⊃ to ⊇, which are rarely used (former: 13 hits, but only in tests/delaborators, latter: 80 hits).

[Floris van Doorn]

Feel free to suggest more abbreviations that you are missing, and I can add them to this PR or a later PR.

[Yaël Dillies]

Can you add \ma so that typing \ma results in ↦ not ♂?

[Yaël Dillies]

Floris van Doorn said:

• \subset from ⊂ to ⊆. The former is almost unused compared to the latter in Mathlib (240 vs 6900 hits). The former symbol is still available as ⊂ or ⊂ This should also make ⊂ autocomplete conveniently to ⊆`

\su already autocompletes to ⊆

[Floris van Doorn]

Yaël Dillies said:

Floris van Doorn said:

• \subset from ⊂ to ⊆. The former is almost unused compared to the latter in Mathlib (240 vs 6900 hits). The former symbol is still available as ⊂ or ⊂ This should also make ⊂ autocomplete conveniently to ⊆`

\su already autocompletes to ⊆

Yes, I know \subs is not the shortest way to write that symbol (although I generally use \sub), but still sometimes I (or a student) occasionally ends up writing.

[Yaël Dillies]

Could you also add \lf for ⌊? It currently gives ⧏

[Floris van Doorn]

I think the first occurrence is chosen in case there are competing matches (and there is no exact match), so I moved the more desirable symbols up.

[Floris van Doorn]

I also added "floor": "⌊$CURSOR⌋" (i.e. you get both symbols and your cursor goes in between).

[Yaël Dillies]

I assume you also added ceil?

[Floris van Doorn]

Of course, adding only one of them would be stupid (quickly pushes a commit adding ceil).

[Eric Wieser]

Should we switch to using ∖ (the unicode) for sdiff?

[Eric Wieser]

Right now it's the only boolean algebra operator that isn't unicode, so I don't think there's that much burden in making it so.

[Yaël Dillies]

Don't see much point in doing so, but we could

[Timo Carlin-Burns]

Yaël Dillies said:

Could you also add \lf for ⌊? It currently gives ⧏

⧏ is currently used as a "less-than-or-fuzzy" relation in SetTheory.PGame. How do you type ⧏ after this change?

[Yaël Dillies]

I don't really mind. Can you come up with an abbreviation that's not lf?

[Timo Carlin-Burns]

\lfuzzy would be acceptable (although it is nice to have symmetry with \le and \lf)

[Yaël Dillies]

I'm afraid ⌊ is much more used than ⧏, so it would be better to respect the \lf/\rf symmetry

[Richard Osborn]

SetTheory.PGame.LF is probably misnamed as well. SetTheory.PGame.LTF or SetTheory.PGame.LTFuzzy seem like more appropriate names.

[Yaël Dillies]

docs#LE would like to disagree :grinning:

[Floris van Doorn]

I renamed \lf to \lfuzzy. \<| is also available. I also added shortcuts for the symmetric symbol ⧐ (maybe also useful for games?)

[Floris van Doorn]

I renamed \lf to \lfuzzy. \<| is also available. I also added shortcuts for the symmetric symbol ⧐ (maybe also useful for games?)