VS Code: `\c[` escape sequence produces `χ[`, not `⦃`

[datokrat]

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The tooltip for ⦃ says that it can be inserted by writing \c[. However, when I write this escape sequence in VS Code or Lean 4 Web, I instead get χ[] (the closing bracket probably being inserted to match [).

Steps to Reproduce

Type \c[ in VS Code or Lean 4 Web.

Expected behavior: [Clear and concise description of what you expect to happen]

The tooltip should only suggest escape sequences that actually work. In this case, typing \c[ should produce ⦃ (and perhaps the closing bracket, too, I don't know).

Actual behavior: [Clear and concise description of what actually happens]

It produces χ[].

Versions

Lean 4.29.0-nightly-2026-02-03
Target: x86_64-unknown-linux-gnu

Additional Information

[Additional information, configuration or data that might be necessary to reproduce the issue]

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[mhuisi]

We should probably just remove these two abbreviations.

[datokrat]

Which second abbreviation will we remove, \{{ (which seems to work as expected)? Wouldn't removing both mean that there is no way to type this bracket on a standard keyboard? It's used in the Std.Do monadic verification framework for Hoare triple notation.

[mhuisi]

\c[ and \c]