Opening an issue at vscode-lean4

Stream: new members

[Doehyun Baek]

Hi. Where should I discuss RFC ideas for vscode-lean4? The issue template says this place is the place for that but I can'tind one.

Specifically, I was wondering if ⟧ can be supported as an abbreviation like (\rrbracket). This is used quite frequenty with denotational semantics and I think it is convenient that it provides only the left option(〚)

[Marc Huisinga]

⟧ is supported with \]] (〚 is \[[). You're right that \rrbracket is missing as an additional abbreviation, though.

[Marc Huisinga]

Ah, it looks like ⟦ (\[[) and 〚 (\llbracket) are different brackets!

[Marc Huisinga]

I've quickly added \rrbracket to the list of abbreviations and it'll be in the next vscode-lean4 release.

[Doehyun Baek]

Oh I actually didn't know that ⟦(\[[) existed. Thanks for the pointer.
Also it seems that \[[ fits my purpose better. Yeah they seem to be two different unicode characters but I myself I'm not sure what the difference actually means.
But I assume addition has no downsides so it seems good.

[Marc Huisinga]

By the way, you can open the list of all available abbreviations by clicking the following button in the top right:
image.png

[Doehyun Baek]

Thanks!