Zulip Chat Archive
Stream: general
Topic: squarish bracket
Patrick Massot (Jan 25 2019 at 22:13):
Does anyone here manages to use https://github.com/leanprover/vscode-lean/blob/master/translations.json#L1036 ? Each time I want to do that VScode inserts a ⟧)
matt rice (Jan 26 2019 at 00:21):
looks like \([) works to get both the left/right squarish, but see the same when trying to get the right alone
Last updated: Dec 20 2023 at 11:08 UTC