How to type ⨍

Stream: lean4

[Geoffrey Irving]

I've forgotten how to type the average integral symbol ⨍ in VSCode. Ideally I'd be able to mouse over it and have it show how to type it, but the mouseover only shows the mathematical description:

Screenshot-2024-01-12-at-9.23.48PM.png

Is this a bug, or is there some other way to get at the keyboard shortcut?

[Julian Berman]

I think the bug is that there isn't actually an abbreviation for it.

[Geoffrey Irving]

That would explain it! I guess I must have just copied and pasted it in the past.

[Kevin Buzzard]

This was also once true for the identity natural transformation (a bold face 1). I'm sure that a PR to abbreviations.json in the lean-vscode repo would be appreciated.

[Kevin Buzzard]

https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4%2Fsrc%2Fabbreviation%2Fabbreviations.json

[Geoffrey Irving]

"average" or "mean"? Happy to send a PR.

[Kevin Buzzard]

you can choose, or add both!

[Geoffrey Irving]

https://github.com/leanprover/vscode-lean4/pull/387. Testing it now.

[Yury G. Kudryashov]

I use \-int locally

[Geoffrey Irving]

Should I still do that PR? If not, is there a way to get that shortcut to show up as a hint?

[Yury G. Kudryashov]

I think that you should make the PR, I suggested one more name motivated by the glyph appearance.

[Yury G. Kudryashov]

While you're on it, could you please also add a shortcut for ∯ (I use oiint locally)

[Yury G. Kudryashov]

It's for docs#torusIntegral

[Yury G. Kudryashov]

Also, I suggest pd for ∂. partial has conflicts with other shortcuts up to parti

[Yury G. Kudryashov]

I wonder if we should cleanup this list and remove the symbols that are never used in Lean+Std4+Mathlib.

[Geoffrey Irving]

I’ll add -int and oiint tomorrow. Though is tint better for torusIntegral?

[Yury G. Kudryashov]

We can have both. oiint is based on LaTeX command.

[Geoffrey Irving]

I added the other abbreviations to the PR, and it's now merged.